Merge lane/t2: matrix reds, C# operators get their own node

Signed-off-by: Martin Vogel <martin.vogel.tech@gmail.com>
This commit is contained in:
Martin Vogel committed 2026-11-01 21:30:26 +01:00
commit 9fb5651ca3
7 files changed
+241 -189

No files matched your search

+9 -3
View File
@@ -866,6 +866,11 @@ TSNode cbm_resolve_func_name(TSNode node, CBMLanguage lang) {
for (int tmpl_depth = 0; tmpl_depth < MAX_TEMPLATE_DEPTH; tmpl_depth++) {
const char *kind = ts_node_type(node);
// C#: an overloaded operator has no name field, its token names it.
if (lang == CBM_LANG_CSHARP && strcmp(kind, "operator_declaration") == 0) {
return ts_node_child_by_field_name(node, TS_FIELD("operator"));
}
if (lang == CBM_LANG_HASKELL && strcmp(kind, "signature") == 0) {
TSNode null_node = {0};
return null_node;
@@ -9291,9 +9296,10 @@ static TSNode resolve_method_name(TSNode child, CBMLanguage lang) {
const char *ck = ts_node_type(child);
if ((lang == CBM_LANG_C || lang == CBM_LANG_CPP || lang == CBM_LANG_CUDA ||
lang == CBM_LANG_GLSL) &&
strcmp(ck, "function_definition") == 0) {
if (((lang == CBM_LANG_C || lang == CBM_LANG_CPP || lang == CBM_LANG_CUDA ||
lang == CBM_LANG_GLSL) &&
strcmp(ck, "function_definition") == 0) ||
(lang == CBM_LANG_CSHARP && strcmp(ck, "operator_declaration") == 0)) {
return cbm_resolve_func_name(child, lang);
}
+14 -1
View File
@@ -864,7 +864,8 @@ static const char *func_kinds_ocaml[] = {"value_definition", "let_binding", NULL
static const char *func_kinds_zig[] = {"function_declaration", "test_declaration", NULL};
static const char *func_kinds_bash[] = {"function_definition", NULL};
static const char *func_kinds_erlang[] = {"function_clause", NULL};
static const char *func_kinds_csharp[] = {"method_declaration", "constructor_declaration", NULL};
static const char *func_kinds_csharp[] = {"method_declaration", "constructor_declaration",
"operator_declaration", NULL};
static const char *func_kinds_matlab[] = {"function_definition", NULL};
static const char *func_kinds_lean[] = {"def", "theorem", "instance", "abbrev", NULL};
static const char *func_kinds_form[] = {"procedure_definition", NULL};
@@ -1203,6 +1204,13 @@ char *cbm_func_name_node_text(CBMArena *a, TSNode name_node, const char *source,
*paren = '\0';
}
}
/* C# `operator +` is named by its token alone, an anonymous node; any other C# name
* is a named node. Spelled like C++'s `operator+` and `operator bool`, here so the
* def name and the call-scope QN cannot disagree. */
if (text && lang == CBM_LANG_CSHARP && !ts_node_is_named(name_node)) {
bool word = text[0] >= 'a' && text[0] <= 'z'; /* operator true, operator false */
return cbm_arena_sprintf(a, "operator%s%s", word ? " " : "", text);
}
/* Nix quoted attrpath segment: `"kebab-case" = a: a;` and `services."my.svc" = …`
* are ordinary names that merely need quoting in source. The node text carries
* the delimiters, so without this the def is named `"kebab-case"` — quotes and
@@ -1493,6 +1501,11 @@ static const char *func_node_name(CBMArena *a, TSNode func_node, const char *sou
if (!ts_node_is_null(name_node)) {
return cbm_node_text(a, name_node, source);
}
// C#: an overloaded operator has no name field, its token names it.
if (lang == CBM_LANG_CSHARP && strcmp(ts_node_type(func_node), "operator_declaration") == 0) {
TSNode op = ts_node_child_by_field_name(func_node, TS_FIELD("operator"));
return ts_node_is_null(op) ? NULL : cbm_func_name_node_text(a, op, source, lang);
}
// Arrow functions: check parent variable_declarator
if (strcmp(ts_node_type(func_node), "arrow_function") == 0) {
TSNode parent = ts_node_parent(func_node);
+4 -4
View File
@@ -369,10 +369,10 @@ static const char *cpp_assign_types[] = {"assignment_expression", "update_expres
static const char *cpp_throw_types[] = {"throw_statement", NULL};
// ==================== C# ====================
static const char *cs_func_types[] = {"destructor_declaration", "local_function_statement",
"function_pointer_type", "constructor_declaration",
"anonymous_method_expression", "lambda_expression",
"method_declaration", NULL};
static const char *cs_func_types[] = {
"destructor_declaration", "local_function_statement", "function_pointer_type",
"constructor_declaration", "anonymous_method_expression", "lambda_expression",
"method_declaration", "operator_declaration", NULL};
static const char *cs_class_types[] = {"class_declaration",
"struct_declaration",
"enum_declaration",
+62 -158
View File
@@ -240,19 +240,10 @@ static const LRP_Golden LRP_GOLDEN[] = {
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_java_s2_method_dispatch", "Runner.java", "Runner.run", "c.inc()", 0, "Counter.java",
"Counter.inc", "CALLS", 5, " public void inc() { n++; }", false, false,
"Typed local Counter receiver exists in source, but package-private Counter fails the "
"public-only owner audit in java_proof_member; same-package visibility needs explicit "
"support.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
"Counter.inc", "CALLS", 5, " public void inc() { n++; }", true, false, NULL, NULL},
{"lrp_java_s2_method_dispatch", "Runner.java", "Runner.run", "c.value()", 0, "Counter.java",
"Counter.value", "CALLS", 6, " public int value() { return n; }", false, false,
"Typed local Counter receiver exists in source, but package-private Counter fails the "
"public-only owner audit in java_proof_member; same-package visibility needs explicit "
"support.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
"Counter.value", "CALLS", 6, " public int value() { return n; }", true, false, NULL,
NULL},
{"lrp_java_s3_constructor", "Factory.java", "Factory.make", "new Widget(name)", 0,
"Widget.java", "Widget.Widget", "CALLS", 5,
" public Widget(String name) { this.name = name; }", false, false,
@@ -270,28 +261,13 @@ static const LRP_Golden LRP_GOLDEN[] = {
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_java_s5_chained", "Main.java", "Main.run", "new Builder().add(1)", 0, "Builder.java",
"Builder.add", "CALLS", 8, " public Builder add(int x) { items.add(x); return this; }",
false, false,
"Fluent construction/return type is not represented by the strict map; java_proof_member "
"accepts only identifier receivers. Nonempty add arguments and package-private owner need "
"separate proof.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
true, false, NULL, NULL},
{"lrp_java_s5_chained", "Main.java", "Main.run", "new Builder().add(1).add(2)", 0,
"Builder.java", "Builder.add", "CALLS", 8,
" public Builder add(int x) { items.add(x); return this; }", false, false,
"Fluent construction/return type is not represented by the strict map; java_proof_member "
"accepts only identifier receivers. Nonempty add arguments and package-private owner need "
"separate proof.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
" public Builder add(int x) { items.add(x); return this; }", true, false, NULL, NULL},
{"lrp_java_s5_chained", "Main.java", "Main.run", "new Builder().add(1).add(2).build()", 0,
"Builder.java", "Builder.build", "CALLS", 9,
" public List<Integer> build() { return items; }", false, false,
"Fluent construction/return type is not represented by the strict map; java_proof_member "
"accepts only identifier receivers. Nonempty add arguments and package-private owner need "
"separate proof.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
" public List<Integer> build() { return items; }", true, false, NULL, NULL},
{"lrp_java_s6_inherited_method", "Dog.java", "Dog.run", "describe()", 0, "Animal.java",
"Animal.describe", "CALLS", 4, " public String describe() { return \"animal\"; }", false,
false,
@@ -307,11 +283,7 @@ static const LRP_Golden LRP_GOLDEN[] = {
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_java_s8_field_type_hint", "Service.java", "Service.run", "logger.log(msg)", 0,
"Logger.java", "Logger.log", "CALLS", 4,
" public void log(String msg) { System.out.println(msg); }", false, false,
"The strict map lacks class-field receiver provenance; Logger is package-private and nonempty "
"String argument applicability is unsupported.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
" public void log(String msg) { System.out.println(msg); }", true, false, NULL, NULL},
{"lrp_csharp_s1_crossfile_call", "Main.cs", "Main.Run", "Util.Square(n)", 0, "Util.cs",
"Util.Square", "CALLS", 3, " public static int Square(int x) { return x * x; }", false,
false,
@@ -320,17 +292,10 @@ static const LRP_Golden LRP_GOLDEN[] = {
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_csharp_s2_method_dispatch", "Runner.cs", "Runner.Run", "c.Inc()", 0, "Counter.cs",
"Counter.Inc", "CALLS", 4, " public void Inc() { n++; }", false, false,
"new Counter() receiver provenance is not added to the strict map; object_creation_expression "
"fails csp_audit and internal Counter/fields also fail the restricted class domain.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
"Counter.Inc", "CALLS", 4, " public void Inc() { n++; }", true, false, NULL, NULL},
{"lrp_csharp_s2_method_dispatch", "Runner.cs", "Runner.Run", "c.Value()", 0, "Counter.cs",
"Counter.Value", "CALLS", 5, " public int Value() { return n; }", false, false,
"new Counter() receiver provenance is not added to the strict map; object_creation_expression "
"fails csp_audit and internal Counter/fields also fail the restricted class domain.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
"Counter.Value", "CALLS", 5, " public int Value() { return n; }", true, false, NULL,
NULL},
{"lrp_csharp_s3_constructor", "Factory.cs", "Factory.Make", "new Widget(name)", 0, "Widget.cs",
"Widget.Widget", "CALLS", 4, " public Widget(string name) { Name = name; }", false,
false,
@@ -347,25 +312,13 @@ static const LRP_Golden LRP_GOLDEN[] = {
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_csharp_s5_chained", "Main.cs", "Main.Run", "new Builder().Add(1)", 0, "Builder.cs",
"Builder.Add", "CALLS", 5, " public Builder Add(int x) { items.Add(x); return this; }",
false, false,
"Constructor/return type propagation and non-identifier fluent receivers are unsupported; "
"object_creation_expression fails body audit and Add has a nonempty argument list.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
true, false, NULL, NULL},
{"lrp_csharp_s5_chained", "Main.cs", "Main.Run", "new Builder().Add(1).Add(2)", 0, "Builder.cs",
"Builder.Add", "CALLS", 5, " public Builder Add(int x) { items.Add(x); return this; }",
false, false,
"Constructor/return type propagation and non-identifier fluent receivers are unsupported; "
"object_creation_expression fails body audit and Add has a nonempty argument list.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
true, false, NULL, NULL},
{"lrp_csharp_s5_chained", "Main.cs", "Main.Run", "new Builder().Add(1).Add(2).Build()", 0,
"Builder.cs", "Builder.Build", "CALLS", 6,
" public List<int> Build() { return items; }", false, false,
"Constructor/return type propagation and non-identifier fluent receivers are unsupported; "
"object_creation_expression fails body audit and Add has a nonempty argument list.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
" public List<int> Build() { return items; }", true, false, NULL, NULL},
{"lrp_csharp_s6_inherited_method", "Child.cs", "Child.Run", "Describe()", 0, "Base.cs",
"Base.Describe", "CALLS", 3, " public virtual string Describe() { return \"base\"; }",
false, false,
@@ -380,11 +333,8 @@ static const LRP_Golden LRP_GOLDEN[] = {
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_csharp_s8_field_type_hint", "Service.cs", "Service.Run", "logger.Log(msg)", 0,
"Logger.cs", "Logger.Log", "CALLS", 3, " public void Log(string msg) { }", false, false,
"Field receiver provenance is missing; csp_function only establishes annotated parameter "
"facts and the nonempty argument needs applicability proof.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
"Logger.cs", "Logger.Log", "CALLS", 3, " public void Log(string msg) { }", true, false,
NULL, NULL},
{"lrp_php_s1_crossfile_call", "main.php", "run", "triple($n)", 0, "util.php", "triple", "CALLS",
2, "function triple($x) { return $x * 3; }", false, false,
"Literal require IMPORTS is proved, but php_proof_calls never resolves "
@@ -572,12 +522,17 @@ static const LRP_Golden LRP_GOLDEN[] = {
"declaration must not be replaced by a name-only target.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
{"lrp_go_usage_struct_literal", "main.go", "Make", "Config", 0, "types.go", "Config", "USAGE",
3, "type Config struct{ Port int }", true, false, NULL, NULL},
{"lrp_go_usage_struct_literal", "main.go", "Make", "Config", 1, "types.go", "Config", "USAGE",
3, "type Config struct{ Port int }", false, false,
"Composite literal type usage is genuine, but generic Go binding validation is unsupported "
"and the strict Go bridge does not publish the struct-literal type occurrence.",
"Prior exact fixture audit: expected target absent; read-only trace of exact fixture and the "
"cited source proof guard. Legacy confidence/name matches were not accepted."},
3, "type Config struct{ Port int }", true, false, NULL, NULL},
/* A key of a struct literal must name a field of that struct (Go spec, composite literals). */
{"lrp_go_usage_struct_literal", "main.go", "Make", "Port", 0, "types.go", "Config.Port", "USAGE",
3, "type Config struct{ Port int }", true, false, NULL, NULL},
{"lrp_go_usage_struct_literal", "main.go", "Make", "Config", 0, "types.go", "Config",
"USES_TYPE", 3, "type Config struct{ Port int }", true, false, NULL, NULL},
{"lrp_go_usage_struct_literal", "main.go", "Make", "Config", 1, "types.go", "Config",
"USES_TYPE", 3, "type Config struct{ Port int }", true, false, NULL, NULL},
{"lrp_ts_usage_type_param", "main.ts", "run", "Config", 1, "types.ts", "Config", "USES_TYPE", 1,
"export interface Config { timeout: number; }", true, false, NULL,
"A parameter annotation is a type use, so USES_TYPE at the exact name; es_usage_crossfile_typescript forbids USAGE here."},
@@ -596,46 +551,17 @@ static const LRP_Golden LRP_GOLDEN[] = {
"The relative-import source proof guard must retain this exact "
"constructor/Class-call regression required."},
{"lrp_java_s2_method_dispatch", "Runner.java", "Runner.run", "new Counter()", 0, "Counter.java",
NULL, "CALLS", 0, NULL, false, false,
"Java supplies a default constructor, but no source constructor declaration exists and "
"projection must not redirect its call to the Class.",
"Source fixture has no constructor declaration; do not invent a Class target or silently omit "
"this semantic invocation from the denominator. A stable implicit declaration identity is "
"needed before an exact graph suffix can be asserted."},
{"lrp_java_s5_chained", "Main.java", "Main.run", "new Builder()", 0, "Builder.java", NULL,
"CALLS", 0, NULL, false, false,
"Java default Builder constructor has no materialized source declaration; this missing "
"constructor identity must remain visible independently of the fluent method misses.",
"Source fixture has no constructor declaration; do not invent a Class target or silently omit "
"this semantic invocation from the denominator. A stable implicit declaration identity is "
"needed before an exact graph suffix can be asserted."},
{"lrp_java_s8_field_type_hint", "Service.java", NULL, "new Logger()", 0, "Logger.java", NULL,
"CALLS", 0, NULL, false, false,
"Implicit constructor invocation occurs in a field initializer, with neither source-declared "
"constructor target nor source-declared initializer callable owner. Needs stable semantic "
"identities for both; do not attach to Service.run.",
"Inspected exact source initializer and absent constructor declaration; no fabricated scope "
"or Class target."},
"Counter", "CALLS", 3, "class Counter {", true, false, NULL, NULL},
{"lrp_java_s5_chained", "Main.java", "Main.run", "new Builder()", 0, "Builder.java", "Builder",
"CALLS", 6, "class Builder {", true, false, NULL, NULL},
{"lrp_java_s8_field_type_hint", "Service.java", "Service.java.__file__", "new Logger()", 0,
"Logger.java", "Logger", "CALLS", 3, "class Logger {", true, false, NULL, NULL},
{"lrp_csharp_s2_method_dispatch", "Runner.cs", "Runner.Run", "new Counter()", 0, "Counter.cs",
NULL, "CALLS", 0, NULL, false, false,
"C# default constructor has no source declaration; needs materialized implicit target "
"identity before an exact CALLS target can exist.",
"Source fixture has no constructor declaration; do not invent a Class target or silently omit "
"this semantic invocation from the denominator. A stable implicit declaration identity is "
"needed before an exact graph suffix can be asserted."},
{"lrp_csharp_s5_chained", "Main.cs", "Main.Run", "new Builder()", 0, "Builder.cs", NULL,
"CALLS", 0, NULL, false, false,
"C# default Builder constructor lacks an explicit source declaration and stable synthetic "
"graph identity.",
"Source fixture has no constructor declaration; do not invent a Class target or silently omit "
"this semantic invocation from the denominator. A stable implicit declaration identity is "
"needed before an exact graph suffix can be asserted."},
{"lrp_csharp_s8_field_type_hint", "Service.cs", NULL, "new Logger()", 0, "Logger.cs", NULL,
"CALLS", 0, NULL, false, false,
"Implicit constructor call appears in a field initializer. Both initializer owner and default "
"constructor target need stable semantic identities; it must not be attributed to "
"Service.Run.",
"Source fixture inspection, no guessed owner/target."},
"Counter", "CALLS", 2, " class Counter {", true, false, NULL, NULL},
{"lrp_csharp_s5_chained", "Main.cs", "Main.Run", "new Builder()", 0, "Builder.cs", "Builder",
"CALLS", 3, " class Builder {", true, false, NULL, NULL},
{"lrp_csharp_s8_field_type_hint", "Service.cs", "Service", "new Logger()", 0, "Logger.cs",
"Logger", "CALLS", 2, " class Logger {", true, false, NULL, NULL},
{"lrp_python_s1_crossfile_call", "main.py", "run", "triple(n)", 0, "util.py", "triple", "CALLS",
1, "def triple(x):", true, false, NULL, NULL},
{"lrp_python_s2_method_dispatch", "main.py", "run", "Counter()", 0, "counter.py", "Counter",
@@ -1037,45 +963,25 @@ static const LRP_Golden LRP_GOLDEN[] = {
"declaration as an incomplete direct member domain; typed receiver alone is insufficient.",
"Reviewed kt_proof_class_fact and direct parameter-type call path; zero-argument method-only "
"classes have positive controls, but this property-bearing fixture does not."},
{"lrp_kotlin_s3_constructor", "Main.kt", "make", "Widget(name)", 0, "Widget.kt", NULL, "CALLS",
0, NULL, false, false,
"The primary constructor is the class header; no independent callable graph identity or "
"Kotlin class-call contract is established. Constructor syntax cannot be promoted by class "
"name alone.",
"kt_proof_function_identity rejects names with type declarations; kt_proof_class_fact also "
"leaves primary-constructor classes incomplete."},
{"lrp_kotlin_s4_companion_static", "App.kt", "run", "Config.default()", 0, "Config.kt", NULL,
"CALLS", 0, NULL, false, false,
"Anonymous companion ownership/materialization and class-to-companion dispatch lack proof.",
"kt_proof_call navigation requires a typed lexical receiver; kt_proof_walk does not walk "
"companion-object declarations. No exact graph QN is invented."},
{"lrp_kotlin_s3_constructor", "Main.kt", "make", "Widget(name)", 0, "Widget.kt", "Widget", "CALLS",
1, "class Widget(val name: String) {", true, false, NULL, NULL},
{"lrp_kotlin_s4_companion_static", "App.kt", "run", "Config.default()", 0, "Config.kt",
"Config.Companion.default", "CALLS", 3, " fun default(): Config = Config(false)",
true, false, NULL, NULL},
{"lrp_kotlin_s4_companion_static", "Config.kt", "Config.Companion.default", "Config(false)", 0,
"Config.kt", NULL, "CALLS", 0, NULL, false, false,
"Primary constructor call within the companion is a separate genuine site; no callable "
"materialization/constructor contract.",
"No Kotlin class-call rule; absence of companion graph scope must remain counted."},
{"lrp_kotlin_s5_chained", "Main.kt", "run", "Builder()", 0, "Builder.kt", NULL, "CALLS", 0,
NULL, false, false, "Implicit primary constructor is not materialized/proven as a callable.",
"Bare function resolution rejects class names; there is no separate constructor producer."},
"Config.kt", "Config", "CALLS", 1, "class Config(val debug: Boolean) {", true, false, NULL,
NULL},
{"lrp_kotlin_s5_chained", "Main.kt", "run", "Builder()", 0, "Builder.kt", "Builder", "CALLS", 1,
"class Builder {", true, false, NULL, NULL},
{"lrp_kotlin_s5_chained", "Main.kt", "run", "Builder().add(1)", 0, "Builder.kt", "Builder.add",
"CALLS", 3, " fun add(x: Int): Builder { items.add(x); return this }", false, false,
"Requires chained constructor/return-type provenance. Navigation proof accepts a simple "
"lexical receiver only; Builder property items also makes class domain incomplete.",
"Reviewed kt_proof_call receiver shape and kt_proof_class_fact. Each add occurrence remains a "
"separate denominator item."},
"CALLS", 3, " fun add(x: Int): Builder { items.add(x); return this }", true, false, NULL,
NULL},
{"lrp_kotlin_s5_chained", "Main.kt", "run", "Builder().add(1).add(2)", 0, "Builder.kt",
"Builder.add", "CALLS", 3, " fun add(x: Int): Builder { items.add(x); return this }", false,
false,
"Requires chained constructor/return-type provenance. Navigation proof accepts a simple "
"lexical receiver only; Builder property items also makes class domain incomplete.",
"Reviewed kt_proof_call receiver shape and kt_proof_class_fact. Each add occurrence remains a "
"separate denominator item."},
"Builder.add", "CALLS", 3, " fun add(x: Int): Builder { items.add(x); return this }", true,
false, NULL, NULL},
{"lrp_kotlin_s5_chained", "Main.kt", "run", "Builder().add(1).add(2).build()", 0, "Builder.kt",
"Builder.build", "CALLS", 4, " fun build(): List<Int> = items.toList()", false, false,
"Requires chained constructor/return-type provenance. Navigation proof accepts a simple "
"lexical receiver only; Builder property items also makes class domain incomplete.",
"Reviewed kt_proof_call receiver shape and kt_proof_class_fact. Each add occurrence remains a "
"separate denominator item."},
"Builder.build", "CALLS", 4, " fun build(): List<Int> = items.toList()", true, false, NULL,
NULL},
{"lrp_kotlin_s6_inherited_method", "Child.kt", "Child.run", "describe()", 0, "Base.kt",
"Base.describe", "CALLS", 2, " open fun describe(): String = \"base\"", false, false,
"Implicit-this inherited member lookup lacks proof; class-context bare calls are disabled and "
@@ -1095,18 +1001,9 @@ static const LRP_Golden LRP_GOLDEN[] = {
"bridge. Unique short name is not authority."},
{"lrp_kotlin_s8_field_type_hint", "Service.kt", "Service.run", "logger.log(msg)", 0,
"Logger.kt", "Logger.log", "CALLS", 2, " fun log(msg: String): Unit { println(msg) }",
false, false,
"Property initializer Logger() does not donate a proven receiver identity to member body; "
"current type map populates declared parameters and callable vals, not class field "
"constructor inference.",
"Reviewed kt_proof_function parameter map and kt_proof_call navigation; constructor and "
"println calls cannot satisfy this method occurrence."},
{"lrp_kotlin_s8_field_type_hint", "Service.kt", "Service", "Logger()", 0, "Logger.kt", NULL,
"CALLS", 0, NULL, false, false,
"Property-initializer constructor invocation lacks callable materialization and initializer "
"scope contract.",
"kt_proof_walk does not publish constructor calls from class property initializers; no Kotlin "
"class-call authority."},
true, false, NULL, NULL},
{"lrp_kotlin_s8_field_type_hint", "Service.kt", "Service", "Logger()", 0, "Logger.kt", "Logger",
"CALLS", 1, "class Logger {", true, false, NULL, NULL},
{"lrp_python_s6b_constructor", "child.py", "run", "Child()", 0, "child.py", "Child", "CALLS", 4,
"class Child(Base):", true, false, NULL,
"Exact imported Class-call identity with CLASS_CALLABLE and occurrence evidence is supported; "
@@ -1314,6 +1211,13 @@ static bool lrp_same_site(const LRP_Check *check, size_t i, uint32_t start, uint
check->pp_starts[i] == start && check->pp_ends[i] == end;
}
/* File and file-level Module nodes identify the whole source, so their persisted
* range is 0/0 (the same convention as rq_target). The row's caller still has to name
* that exact node; any other scope must enclose the occurrence. */
static bool lrp_scope_encloses(int first, int last, int line) {
return (first == 0 && last == 0) || (first <= line && last >= line);
}
/* Do not prefilter by the expected span, scope or role: a shifted/rebound
* occurrence must fail rather than become a tolerated missing edge. */
static bool lrp_match_occurrence(LRP_Check *check, sqlite3_stmt *stmt) {
@@ -1340,8 +1244,8 @@ static bool lrp_match_occurrence(LRP_Check *check, sqlite3_stmt *stmt) {
continue;
bool identity = source_file && !strcmp(source_file, g->file) &&
lrp_qn_has_declaration(scope, g->caller) &&
sqlite3_column_int(stmt, 11) <= check->lines[i] &&
sqlite3_column_int(stmt, 12) >= check->lines[i] &&
lrp_scope_encloses(sqlite3_column_int(stmt, 11),
sqlite3_column_int(stmt, 12), check->lines[i]) &&
lrp_target_matches(g, target_file, target, sqlite3_column_int(stmt, 8),
sqlite3_column_int(stmt, 9));
if (identity && g->forbidden) {
+126 -16
View File
@@ -133,9 +133,9 @@ static void mkc_cleanup(MKC_Proj *lp, cbm_store_t *store) {
/* Each obligation below is authored from its fixture, independently of emitted
* rows. Missing edges remain quality debt; invented targets fail the oracle.
* Unsupported implicit constructors retain a real source declaration anchor
* with no fabricated callable identity. The explicit C# operator also retains
* its unmapped callable identity as debt. Unknown receiver sites are forbidden. */
* A class stands for a constructor that has no node of its own: a primary constructor
* in the class header, a synthesized apply, or a Swift init. The evidence marks it as a
* class call. Unknown receiver sites are forbidden. */
typedef struct {
const char *test, *caller, *needle, *target, *declaration, *label;
int line;
@@ -143,14 +143,14 @@ typedef struct {
bool required;
} MKC_Golden;
static const MKC_Golden mkc_goldens[] = {
{"mkc_c1_scala_constructor_new", "make", "new Widget(n)", NULL,
"class Widget(val name: String) {", "Method", 1, 0, false},
{"mkc_c1_scala_case_class_apply", "origin", "Point(0.0, 0.0)", NULL,
"case class Point(x: Double, y: Double) {", "Method", 1, 0, false},
{"mkc_c1_scala_constructor_new", "make", "new Widget(n)", "Widget",
"class Widget(val name: String) {", "Class", 1, 0, true},
{"mkc_c1_scala_case_class_apply", "origin", "Point(0.0, 0.0)", "Point",
"case class Point(x: Double, y: Double) {", "Class", 1, 0, true},
{"mkc_c1_scala_case_class_apply", "origin", "Point(0.0, 0.0).dist()", "dist",
" def dist(): Double = math.sqrt(x*x + y*y)", "Method", 2, 0, true},
{"mkc_c1_swift_initializer", "make", "Widget(name: n)", "init",
" init(name: String) { self.name = name }", "Method", 3, 0, false},
{"mkc_c1_swift_initializer", "make", "Widget(name: n)", "Widget", "class Widget {", "Class", 1, 0,
true},
{"mkc_c1_ruby_type_new", "make", "Widget.new(name)", "initialize", " def initialize(name)",
"Method", 2, 0, true},
{"mkc_c1_rust_new_samefile", "run", "Point::new(3.0, 4.0)", "new",
@@ -177,12 +177,12 @@ static const MKC_Golden mkc_goldens[] = {
"Method", 8, 0, false},
{"mkc_c2_kotlin_operator_plus", "run", "a + b", "plus",
" operator fun plus(other: Vec2): Vec2 =", "Method", 2, 0, true},
{"mkc_c2_csharp_operator_plus", "Run", "a + b", NULL,
{"mkc_c2_csharp_operator_plus", "Run", "a + b", "operator+",
" public static Vec2 operator+(Vec2 a, Vec2 b) {", "Method", 5, 0, false},
{"mkc_c2_csharp_operator_plus", "Run", "(a + b).Dot(b)", "Dot",
" public float Dot(Vec2 o) { return X*o.X + Y*o.Y; }", "Method", 8, 0, false},
{"mkc_c2_csharp_operator_plus", "operator+", "new Vec2(a.X + b.X, a.Y + b.Y)", "Vec2",
" public Vec2(float x, float y) { X = x; Y = y; }", "Method", 4, 0, false},
" public Vec2(float x, float y) { X = x; Y = y; }", "Method", 4, 0, true},
{"mkc_c2_scala_symbolic_method", "run", "a + b", "+",
" def +(other: Vec2): Vec2 = Vec2(x + other.x, y + other.y)", "Method", 2, 0, false},
{"mkc_c2_scala_symbolic_method", "run", "(a + b).dot(b)", "dot",
@@ -258,13 +258,30 @@ static const MKC_Golden mkc_goldens[] = {
" make(name: string): Widget { return new Widget(name); }", "Method", 7, 0, true},
{"mkc_c8_typescript_constructor_samefile", "run", "this.make(name).label()", "label",
" label(): string { return this.name; }", "Method", 3, 0, false},
{"mkc_c8_kotlin_constructor_samefile", "make", "Widget(name)", NULL,
"class Widget(val name: String) {", "Method", 1, 0, false},
{"mkc_c8_kotlin_constructor_samefile", "make", "Widget(name)", "Widget",
"class Widget(val name: String) {", "Class", 1, 0, true},
{"mkc_c8_kotlin_constructor_samefile", "run", "make(name)", "make",
"fun make(name: String): Widget = Widget(name)", "Function", 5, 0, true},
{"mkc_c8_kotlin_constructor_samefile", "run", "make(name).label()", "label",
" fun label(): String = name", "Method", 2, 0, true},
};
/* The harness audits a known target under every role. A class named in a signature is
* referenced there, in these languages as USAGE and as USES_TYPE, apart from the call. */
typedef struct {
const char *test, *caller, *needle, *relation, *target, *declaration;
int line;
unsigned occurrence;
} MKC_TypeMention;
static const MKC_TypeMention mkc_type_mentions[] = {
{"mkc_c1_scala_constructor_new", "make", "Widget", "USAGE", "Widget",
"class Widget(val name: String) {", 1, 1},
{"mkc_c1_scala_constructor_new", "make", "Widget", "USES_TYPE", "Widget",
"class Widget(val name: String) {", 1, 1},
{"mkc_c1_swift_initializer", "make", "Widget", "USAGE", "Widget", "class Widget {", 1, 1},
{"mkc_c1_swift_initializer", "make", "Widget", "USES_TYPE", "Widget", "class Widget {", 1, 1},
{"mkc_c8_kotlin_constructor_samefile", "make", "Widget", "USAGE", "Widget",
"class Widget(val name: String) {", 1, 1},
};
typedef struct {
const char *test, *caller, *needle;
unsigned occurrence;
@@ -327,9 +344,7 @@ static bool mkc_quality(const MKC_File *original, int count, const char *test) {
.why = g->target
? "This source-authored call requires a complete language binding and "
"receiver/overload proof to its exact callable declaration."
: "The genuine call has no faithful callable graph identity. A class "
"anchor for an implicit constructor, or an explicit operator anchor, "
"records debt without accepting a Class as a callable target.",
: "The genuine call has no faithful callable graph identity.",
.tried = "The original v69 production harness failed its aggregate call floor. "
"Preserved fixture bytes and replaced that floor with exact source "
"occurrences/declarations. Direct make calls remain required source "
@@ -342,6 +357,28 @@ static bool mkc_quality(const MKC_File *original, int count, const char *test) {
required += g->required;
n++;
}
for (size_t i = 0; i < sizeof(mkc_type_mentions) / sizeof(mkc_type_mentions[0]); i++) {
const MKC_TypeMention *g = mkc_type_mentions + i;
if (strcmp(test, g->test))
continue;
if (n == sizeof(expected) / sizeof(expected[0]))
return false;
snprintf(ids[n], sizeof(ids[n]), "%s-%zu", test, n);
expected[n] = (RQ_Expected){.case_id = ids[n],
.site = {.file = original[0].name,
.caller = g->caller,
.needle = g->needle,
.occurrence_index = g->occurrence},
.relation = g->relation,
.target = {.file = original[0].name,
.suffix = g->target,
.label = "Class",
.declaration_line = g->line,
.declaration_text = g->declaration},
.mode = RQ_REQUIRED};
required++;
n++;
}
for (size_t i = 0; i < sizeof(mkc_forbidden) / sizeof(mkc_forbidden[0]); i++) {
const MKC_Forbidden *g = mkc_forbidden + i;
if (strcmp(test, g->test))
@@ -657,6 +694,78 @@ TEST(mkc_c2_csharp_operator_plus) {
PASS();
}
/* A C# operator's body has its own node, also when the operator is overloaded or spelled
* with a space or a word. A call in it belongs to that operator, never to the file. */
TEST(mkc_c2_csharp_operator_overloads) {
static const char source[] =
"namespace App {\n"
" struct Vec2 {\n"
" public float X;\n"
" public Vec2(float x) { X = x; }\n"
" public static Vec2 operator+(Vec2 a, Vec2 b) { return new Vec2(a.X + b.X); }\n"
" public static Vec2 operator+(Vec2 a, float b) { return new Vec2(a.X + b); }\n"
" public static Vec2 operator -(Vec2 a, Vec2 b) { return new Vec2(a.X - b.X); }\n"
" public static bool operator true(Vec2 a) { return Check(a); }\n"
" static bool Check(Vec2 a) { return true; }\n"
" }\n"
"}\n";
const MKC_File files[] = {{"Vec.cs", source}};
const RQ_Source sources[] = {{.path = "Vec.cs", .text = source}};
const RQ_Target ctor = {.file = "Vec.cs",
.suffix = "Vec2.Vec2",
.label = "Method",
.declaration_line = 4,
.declaration_text = " public Vec2(float x) { X = x; }"};
const RQ_Target check = {.file = "Vec.cs",
.suffix = "Vec2.Check",
.label = "Method",
.declaration_line = 9,
.declaration_text =
" static bool Check(Vec2 a) { return true; }"};
const RQ_Expected expected[] = {
{.case_id = "first-plus",
.site = {.file = "Vec.cs",
.caller = "Vec2.operator+",
.needle = "new Vec2(a.X + b.X)",
.caller_variant_start_line = 5,
.caller_variant_end_line = 5,
.caller_variant_declaration = " public static Vec2 operator+(Vec2 a, Vec2 "
"b) { return new Vec2(a.X + b.X); }"},
.relation = "CALLS",
.target = ctor,
.mode = RQ_REQUIRED},
{.case_id = "second-plus",
.site = {.file = "Vec.cs",
.caller = "Vec2.operator+",
.needle = "new Vec2(a.X + b)",
.caller_variant_start_line = 6,
.caller_variant_end_line = 6,
.caller_variant_declaration = " public static Vec2 operator+(Vec2 a, float "
"b) { return new Vec2(a.X + b); }"},
.relation = "CALLS",
.target = ctor,
.mode = RQ_REQUIRED},
{.case_id = "minus",
.site = {.file = "Vec.cs", .caller = "Vec2.operator-", .needle = "new Vec2(a.X - b.X)"},
.relation = "CALLS",
.target = ctor,
.mode = RQ_REQUIRED},
{.case_id = "word",
.site = {.file = "Vec.cs", .caller = "Vec2.operator true", .needle = "Check(a)"},
.relation = "CALLS",
.target = check,
.mode = RQ_REQUIRED}};
MKC_Proj project;
cbm_store_t *store = mkc_index(&project, files, 1);
RQ_Report report = {0};
bool ok = store && rq_check_project_declarations(store, project.project, __func__, sources, 1,
expected, 4, NULL, 0, &report, stderr);
mkc_cleanup(&project, store);
ASSERT_TRUE(ok);
ASSERT_EQ(report.found, 4);
PASS();
}
/* c2 scala symbolic method: exact source calls are required obligations or named quality gaps;
* unknown receiver sites cannot bind to a same-named project method. */
TEST(mkc_c2_scala_symbolic_method) {
@@ -1309,6 +1418,7 @@ SUITE(matrix_known_classes) {
RUN_TEST(mkc_c2_kotlin_operator_plus);
/* C2-G: C# operator+ — red=bug */
RUN_TEST(mkc_c2_csharp_operator_plus);
RUN_TEST(mkc_c2_csharp_operator_overloads);
/* C2-H: Scala symbolic method — uncertain/red=bug */
RUN_TEST(mkc_c2_scala_symbolic_method);
/* C2-I: Ruby def + — uncertain/red=bug */
+24 -5
View File
@@ -249,8 +249,8 @@ static const MN_Golden mn_goldens[] = {
" pub fn enqueue(&mut self, item: T) { self.buf.push_back(item); }", "Method", 7, 0, true},
{"mn_extension_rust_impl", "demo", "q.dequeue()", "dequeue",
" pub fn dequeue(&mut self) -> Option<T> { self.buf.pop_front() }", "Method", 8, 0, true},
{"mn_record_kotlin_data_class", "anon", "User(\"anon\", 0)", NULL,
"data class User(val name: String, val age: Int) {", "Method", 1, 0, false},
{"mn_record_kotlin_data_class", "anon", "User(\"anon\", 0)", "User",
"data class User(val name: String, val age: Int) {", "Class", 1, 0, true},
{"mn_record_kotlin_data_class", "run", "User.anon()", "anon",
" fun anon(): User = User(\"anon\", 0)", "Method", 6, 0, true},
{"mn_record_kotlin_data_class", "run", "User.anon().greet()", "greet",
@@ -402,9 +402,9 @@ static bool mn_quality(const char *test, const char *filename, const char *conte
g->target
? "Generic/conditional, namespace or effectful value binding needs a complete "
"proof to this independently authored callable declaration."
: "The genuine invocation targets a returned closure or implicit constructor. "
"Its source anchor records the missing callable identity without accepting "
"a variable or class node as the target.",
: "The genuine invocation targets a returned closure. Its source anchor "
"records the missing callable identity without accepting a variable node "
"as the target.",
.tried = "The original full production harness failed its v69 call floor. Original "
"source bytes and structural assertions remain intact; each covered caller "
"now enumerates its project call sites and a required control checks the "
@@ -414,6 +414,25 @@ static bool mn_quality(const char *test, const char *filename, const char *conte
}
if (n == 1)
return false;
/* The harness audits a known target under every role: `anon(): User` names the class
* it also constructs, and that signature is a USAGE of it. */
if (!strcmp(test, "mn_record_kotlin_data_class")) {
if (n == sizeof(expected) / sizeof(expected[0]))
return false;
snprintf(ids[n], sizeof(ids[n]), "%s-%zu", test, n);
expected[n] = (RQ_Expected){
.case_id = ids[n],
.site = {.file = filename, .caller = "anon", .needle = "User", .occurrence_index = 1},
.relation = "USAGE",
.target = {.file = filename,
.suffix = "User",
.label = "Class",
.declaration_line = 1,
.declaration_text = "data class User(val name: String, val age: Int) {"},
.mode = RQ_REQUIRED};
required++;
n++;
}
MN_LangProj lp;
cbm_store_t *store = mn_index_files(&lp, files, 2);
RQ_Report report = {0};
+2 -2
View File
@@ -1051,7 +1051,7 @@ TEST(probe_kotlin_data_class) {
ASSERT_TRUE(m.functions + m.methods >= 2);
ASSERT_TRUE(m.quality_ok);
ASSERT_EQ(m.quality.genuine, sizeof(expected) / sizeof(expected[0]));
ASSERT_EQ(m.quality.missing, sizeof(expected) / sizeof(expected[0]));
ASSERT_EQ(m.quality.missing, 0);
ASSERT_EQ(m.quality.wrong, 0);
PASS();
}
@@ -1158,7 +1158,7 @@ TEST(probe_cs_class_methods) {
ASSERT_TRUE(m.methods >= 2); /* Add, Double */
ASSERT_TRUE(m.quality_ok);
ASSERT_EQ(m.quality.genuine, sizeof(expected) / sizeof(expected[0]));
ASSERT_EQ(m.quality.missing, sizeof(expected) / sizeof(expected[0]));
ASSERT_EQ(m.quality.missing, 0);
ASSERT_EQ(m.quality.wrong, 0);
PASS();
}