From cf3a546130e9afd37cc19dc7694dae2fe6a7181f Mon Sep 17 00:00:00 2001 From: Sung-Shik Jongmans Date: Wed, 13 May 2026 14:27:36 +0200 Subject: [PATCH 1/4] Add `define2id` property to `TModel` as a level of indirection to make use-defs more precise --- src/analysis/typepal/Collector.rsc | 26 +++++++++++++++++++++++--- src/analysis/typepal/ICollector.rsc | 4 ++-- src/analysis/typepal/Solver.rsc | 4 ++-- src/analysis/typepal/TModel.rsc | 1 + 4 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/analysis/typepal/Collector.rsc b/src/analysis/typepal/Collector.rsc index 872093cf..2f3cd76d 100644 --- a/src/analysis/typepal/Collector.rsc +++ b/src/analysis/typepal/Collector.rsc @@ -204,6 +204,8 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co Defines defines = {}; Defines addedDefines = {}; + map[loc,loc] define2id = (); + map[loc,loc] logical2physical = (); map[loc,loc] physical2logical = (); @@ -250,12 +252,21 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co bool building = true; - void collector_define(str orgId, IdRole idRole, value def, DefInfo info){ + void collector_define(value id, IdRole idRole, value def, DefInfo info){ if(building){ loc l = |undefined:///|; if(Tree tdef := def) l = getLoc(tdef); else if(loc ldef := def) l = ldef; else throw TypePalUsage("Argument `def` of `define` should be `Tree` or `loc`, found "); + + str orgId = ""; + if(Tree tid := id) { + orgId = ""; + define2id[l] = tid.src; + } + else if(str sid := id) orgId = sid; + else throw TypePalUsage("Argument `id` of `define` should be `Tree` or `str`, found "); + nname = normalizeName(orgId); Define newDef = ; logL = buildLogical2physical(newDef); @@ -323,7 +334,7 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co return false; } - void collector_defineInScope(value scope, str orgId, IdRole idRole, value def, DefInfo info){ + void collector_defineInScope(value scope, value id, IdRole idRole, value def, DefInfo info){ if(building){ loc definingScope = |undefined:///|; if(Tree tscope := scope) definingScope = getLoc(tscope); @@ -335,6 +346,14 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co else if(loc ldef := def) l = ldef; else throw TypePalUsage("Argument `def` of `defineInScope` should be `Tree` or `loc`, found "); + str orgId = ""; + if(Tree tid := id) { + orgId = ""; + define2id[l] = tid.src; + } + else if(str sid := id) orgId = sid; + else throw TypePalUsage("Argument `id` of `defineInScope` should be `Tree` or `str`, found "); + nname = normalizeName(orgId); Define newDef = ; logL = buildLogical2physical(newDef); @@ -1011,7 +1030,8 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co } tm.definesMap = definesMap; definesMap = (); defines = addedDefines = {}; - + tm.define2id = define2id; define2id = (); + tm.scopes = toLogicalLocs(scopes - addedScopes) + addedScopes; scopes = addedScopes = (); tm.paths = toLogicalLocs(paths - addedPaths) + addedPaths; paths = addedPaths = {}; tm.referPaths = toLogicalLocs(referPaths); referPaths = {}; diff --git a/src/analysis/typepal/ICollector.rsc b/src/analysis/typepal/ICollector.rsc index d5df681d..dd042614 100644 --- a/src/analysis/typepal/ICollector.rsc +++ b/src/analysis/typepal/ICollector.rsc @@ -47,8 +47,8 @@ data Collector /* Reporting */ bool (FailMessage msg) report, bool (list[FailMessage] msgs) reports, - /* Define */ void (str id, IdRole idRole, value def, DefInfo info) define, - void (value scope, str id, IdRole idRole, value def, DefInfo info) defineInScope, + /* Define */ void (value id, IdRole idRole, value def, DefInfo info) define, + void (value scope, value id, IdRole idRole, value def, DefInfo info) defineInScope, Tree (str id, IdRole idRole, value def, DefInfo info) predefine, Tree (value scope, str id, IdRole idRole, DefInfo info) predefineInScope, bool (str id, Tree useOrDef) isAlreadyDefined, diff --git a/src/analysis/typepal/Solver.rsc b/src/analysis/typepal/Solver.rsc index 1dfc726f..cdff123f 100644 --- a/src/analysis/typepal/Solver.rsc +++ b/src/analysis/typepal/Solver.rsc @@ -819,7 +819,7 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){ Define solver_getDefine(loc l) = definitions[getLogicalLoc(l)]; rel[loc,loc] solver_getUseDef() - = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; + = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; bool solver_isContainedIn(loc inner, loc outer) = isContainedIn(inner, outer, logical2physical); @@ -1653,7 +1653,7 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){ tm.specializedFacts = specializedFacts; //println("definedBy;"); iprintln(definedBy); - tm.useDef = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; + tm.useDef = solver_getUseDef(); ldefines = for(tup: <- tm.defines){ if(defInfo has tree){ diff --git a/src/analysis/typepal/TModel.rsc b/src/analysis/typepal/TModel.rsc index d13feeb5..c95bb85c 100644 --- a/src/analysis/typepal/TModel.rsc +++ b/src/analysis/typepal/TModel.rsc @@ -115,6 +115,7 @@ data TModel ( map[loc, Define] definitions = (), map[loc,loc] logical2physical = (), bool usesPhysicalLocs = false, // Are locations in physical format? + map[loc,loc] define2id = (), TypePalConfig config = tconfig() ) = tmodel(); From e007df41844aa5d9413e35b1f363d4f1d236b9e2 Mon Sep 17 00:00:00 2001 From: Sung-Shik Jongmans Date: Wed, 13 May 2026 14:28:45 +0200 Subject: [PATCH 2/4] Update FWJ example to compute more precise use-defs --- src/examples/fwjava/Checker.rsc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/examples/fwjava/Checker.rsc b/src/examples/fwjava/Checker.rsc index a2c21230..0b4f7180 100644 --- a/src/examples/fwjava/Checker.rsc +++ b/src/examples/fwjava/Checker.rsc @@ -102,7 +102,7 @@ TypePalConfig fwjConfig() = // ---- Collect -------------------------------------------------------------- void collect(current: (ClassDecl) `class extends { }`, Collector c) { - c.define("", classId(), current, defType(classType(""))); + c.define(cid, classId(), current, defType(classType(""))); c.enterScope(current); c.push(key_extendsRelation, <"", "">); scope = c.getScope(); @@ -131,22 +131,22 @@ void collect(current: (ConstructorDecl ) ` { ", "")); c.enterScope(current); tp = methodType(classType(""), atypeList([classType("") | Formal f <- formals.formals])); - c.defineInScope(scope, "", constructorId(), current, defType(tp)); + c.defineInScope(scope, cid, constructorId(), current, defType(tp)); collect(formals, superCall, fieldAssignments, c); c.leaveScope(current); } void collect(current: (Formal) ` `, Collector c){ - c.define("", formalId(), current, defType(classType(""))); + c.define(id, formalId(), current, defType(classType(""))); } void collect(fd: (FieldDecl) ` ;`, Collector c){ - c.define("", fieldId(), id, defType(classType(""))); + c.define(id, fieldId(), id, defType(classType(""))); } void collect(current: (MethodDecl) ` { return ; }`, Collector c){ formal_list = [formal | formal <- formals.formals]; - c.define("", methodId(), current, defType(formal_list + exp, AType(Solver s) { return methodType(s.getType(exp), atypeList([s.getType(formal) | formal <- formal_list])); })); + c.define(mid, methodId(), current, defType(formal_list + exp, AType(Solver s) { return methodType(s.getType(exp), atypeList([s.getType(formal) | formal <- formal_list])); })); c.enterScope(current); c.requireSubType(exp, classType(""), error(current, "Actual return type %t should be subtype of declared return type %t", exp, cid)); collect(formals, exp, c); From 88904ffc54f94ff4e256887a0f64940a5d51c4dd Mon Sep 17 00:00:00 2001 From: Sung-Shik Jongmans Date: Tue, 9 Jun 2026 13:48:27 +0200 Subject: [PATCH 3/4] Add basic use-def test for the FWJ examples to check if more precise use-defs are computed --- src/analysis/typepal/Solver.rsc | 6 +++++- src/examples/fwjava/Test.rsc | 15 ++++++++++++--- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/analysis/typepal/Solver.rsc b/src/analysis/typepal/Solver.rsc index 980be145..86e35f33 100644 --- a/src/analysis/typepal/Solver.rsc +++ b/src/analysis/typepal/Solver.rsc @@ -62,6 +62,10 @@ void assertValidUseDef(TModel tm, Solver solver) { useLocs = sort([u.occ | u <- tm.uses], isLexicallyLess); defLocs = sort([d.defined | d <- tm.defines], isLexicallyLess); for (pair: <- tm.useDef) { + // Invert `define2id` when needed + if (/Define d := tm.defines, defLoc == (tm.define2id[d.defined] ? |unknown:///|)) { + defLoc = d.defined; + } assert useLoc in useLocs : "Expected: For each `\` in `tm.useDef`, a corresponding `Use` exists in `tm.uses` for `useLoc`. " + @@ -956,7 +960,7 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){ Define solver_getDefine(loc l) = definitions[getLogicalLoc(l)]; rel[loc,loc] solver_getUseDef() - = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; + = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; bool solver_isContainedIn(loc inner, loc outer) = isContainedIn(inner, outer, logical2physical); diff --git a/src/examples/fwjava/Test.rsc b/src/examples/fwjava/Test.rsc index e62bfe4b..44423cda 100644 --- a/src/examples/fwjava/Test.rsc +++ b/src/examples/fwjava/Test.rsc @@ -45,9 +45,18 @@ test bool fwjTModelTestCpt() = [] := fwjTModelFromName("cpt", false).messages; test bool fwjTModelTestPair() = [] := fwjTModelFromName("pair", false).messages; test bool fwjTModelTestTmp() = [_, _] := fwjTModelFromName("tmp", false).messages; // Two errors expected -test bool fwjUseDefTestCpt() { - tm = fwjTModelFromName("cpt", false); - iprintln(tm.useDef); +test bool fwjUseDefTestCpt() = fwjUseDefTest("cpt"); +test bool fwjUseDefTestPair() = fwjUseDefTest("pair"); +test bool fwjUseDefTestTmp() = fwjUseDefTest("tmp"); + +private bool fwjUseDefTest(str name) { + tm = fwjTModelFromName(name, false); + for ( <- tm.useDef, u.length?, d.length?) { + // The following assertion is an indirect, but automatic/simple, + // approximation to check if `d` is the location of the identifier of a + // definition (instead of the whole definition). + assert u.length == d.length; + } return true; } From 06de355a2adf80e53c74fdba56ce67e7bcb12002 Mon Sep 17 00:00:00 2001 From: Sung-Shik Jongmans Date: Tue, 9 Jun 2026 15:50:25 +0200 Subject: [PATCH 4/4] Fix issue that logical locations weren't resolved properly yet through `define2id` --- src/analysis/typepal/Solver.rsc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analysis/typepal/Solver.rsc b/src/analysis/typepal/Solver.rsc index 86e35f33..2a118e95 100644 --- a/src/analysis/typepal/Solver.rsc +++ b/src/analysis/typepal/Solver.rsc @@ -960,7 +960,10 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){ Define solver_getDefine(loc l) = definitions[getLogicalLoc(l)]; rel[loc,loc] solver_getUseDef() - = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; + = { *{ | loc d <- definedBy[u]} | loc u <- definedBy }; + + loc resolveDef(loc def) + = tm.define2id[tm.logical2physical[def] ? def] ? def; bool solver_isContainedIn(loc inner, loc outer) = isContainedIn(inner, outer, logical2physical);