More precise use-defs

src/analysis/typepal/Collector.rsc

@@ -215,6 +215,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 = ();
@@ -261,12 +263,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 <typeOf(def)>");
+
+            str orgId = "";
+            if(Tree tid := id) {
+                orgId = "<tid>";
+                define2id[l] = tid.src;
+            }
+            else if(str sid := id) orgId = sid;
+            else throw TypePalUsage("Argument `id` of `define` should be `Tree` or `str`, found <typeOf(orgId)>");
+
             nname = normalizeName(orgId);
             Define newDef = <currentScope, nname, orgId, idRole, l, info>;
             logL = buildLogical2physical(newDef);
@@ -334,7 +345,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);
@@ -346,6 +357,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 <typeOf(def)>");
 
+            str orgId = "";
+            if(Tree tid := id) {
+                orgId = "<tid>";
+                define2id[l] = tid.src;
+            }
+            else if(str sid := id) orgId = sid;
+            else throw TypePalUsage("Argument `id` of `defineInScope` should be `Tree` or `str`, found <typeOf(orgId)>");
+
             nname = normalizeName(orgId);
             Define newDef = <definingScope, nname, orgId, idRole, l, info>;
             logL = buildLogical2physical(newDef);
@@ -1022,7 +1041,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 = {};

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,

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: <useLoc, defLoc> <- 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 `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Use` exists in `tm.uses` for `useLoc`. " +
@@ -956,7 +960,10 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
     Define solver_getDefine(loc l) = definitions[getLogicalLoc(l)];
 
     rel[loc,loc] solver_getUseDef()
-        = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
+        = { *{<u, resolveDef(d)> | 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);
@@ -1790,7 +1797,7 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         tm.specializedFacts = specializedFacts;
 
         //println("definedBy;"); iprintln(definedBy);
-        tm.useDef = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
+        tm.useDef = solver_getUseDef();
 
         // Update `uses` with all uses resolved by the solver
         tm.uses = [*({*tm.uses} + {*def2uses[d] | d <- def2uses})];

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();
 

src/examples/fwjava/Checker.rsc

@@ -102,7 +102,7 @@ TypePalConfig fwjConfig() =
 // ----  Collect --------------------------------------------------------------
 
 void collect(current: (ClassDecl) `class <ClassId cid> extends <ClassId ecid> { <FieldDecl* fieldDecls> <ConstructorDecl constructorDecl> <MethodDecl* methodDecls> }`, Collector c) {
-    c.define("<cid>", classId(), current, defType(classType("<cid>")));
+    c.define(cid, classId(), current, defType(classType("<cid>")));
     c.enterScope(current);
         c.push(key_extendsRelation, <"<cid>", "<ecid>">);
         scope = c.getScope();
@@ -131,22 +131,22 @@ void collect(current: (ConstructorDecl ) `<ClassId cid> <Formals formals> { <Sup
         c.report(error(current, "Expected constructor name %q, found %q", "<cid1>", "<cid>"));
     c.enterScope(current);
         tp = methodType(classType("<cid1>"), atypeList([classType("<f.cid>") | Formal f <- formals.formals]));
-        c.defineInScope(scope, "<cid>", constructorId(), current, defType(tp));
+        c.defineInScope(scope, cid, constructorId(), current, defType(tp));
         collect(formals, superCall, fieldAssignments, c);
     c.leaveScope(current);            
 }
 
 void collect(current: (Formal) `<ClassId cid> <Id id>`, Collector c){
-     c.define("<id>", formalId(), current, defType(classType("<cid>")));   
+     c.define(id, formalId(), current, defType(classType("<cid>")));   
 }
 
 void collect(fd: (FieldDecl) `<ClassId cid> <Id id> ;`, Collector c){
-     c.define("<id>", fieldId(), id, defType(classType("<cid>")));
+     c.define(id, fieldId(), id, defType(classType("<cid>")));
 }
 
 void collect(current: (MethodDecl) `<ClassId cid> <Id mid> <Formals formals> { return <Expression exp> ; }`,  Collector c){   
      formal_list =  [formal | formal <- formals.formals];
-     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.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("<cid>"), error(current,  "Actual return type %t should be subtype of declared return type %t", exp, cid));
          collect(formals, exp, c);

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 (<u, d> <- 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;
 }