Validation of tm.defines and tm.useDef

src/analysis/typepal/ConfigurableScopeGraph.rsc

@@ -108,6 +108,9 @@ data TypePalConfig(
         );
 
 data TypePalConfig(
+        bool assertValidDefines = false,
+        bool assertValidUseDef  = false,
+
         bool verbose               = false,
 
         PathConfig typepalPathConfig = pathConfig(),

src/analysis/typepal/Solver.rsc

@@ -40,6 +40,63 @@ void checkAllTypesAvailable(TModel tm){
     }
 }
 
+void assertValidDefines(TModel tm){
+    if (!tm.config.assertValidDefines) return;
+    for(d <- tm.defines){
+
+        assert isContainedIn(d.defined, d.scope, tm.logical2physical) || "global-scope" == d.scope.scheme : 
+            "Expected: For each `d` in `tm.defines`, `d.defined` is contained in `d.scope`. " +
+            "Actual: For `<d>` in TModel `<tm.modelName>`, `<d.defined>` (`d.defined`) isn\'t contained in `<d.scope>` (`d.scope`).";
+
+        assert d.defInfo has atype : 
+            "Expected: For each `d` in `tm.defines`, field `d.defInfo` has field `atype`. " +
+            "Actual: For `<d>` in TModel `<tm.modelName>`, `<d.defInfo>` (`d.defInfo`) doesn\'t have that field.";
+    }
+}
+
+void assertValidUseDef(TModel tm, Solver solver) {
+    if (!tm.config.assertValidUseDef) return;
+    scopeGraph = newScopeGraph(tm, tm.config);
+    scopeGraph.setSolver(solver);
+
+    useLocs = sort([u.occ | u <- tm.uses], isLexicallyLess);
+    defLocs = sort([d.defined | d <- tm.defines], isLexicallyLess);
+    for (pair: <useLoc, defLoc> <- tm.useDef) {
+
+        assert useLoc in useLocs :
+            "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Use` exists in `tm.uses` for `useLoc`. " +
+            "Actual: For `<pair>` in TModel `<tm.modelName>`, a corresponding `Use` value doesn\'t exist for `<useLoc>` (`useLoc`), but it does for `<useLocs>`.";
+
+        assert defLoc in defLocs :
+            "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Define` exists in `tm.defines` for `defLoc`. " +
+            "Actual: For `<pair>` in TModel `<tm.modelName>`, a corresponding `Define` value doesn\'t exist for `<defLoc>` (`defLoc`), but it does for `<defLocs>`.";
+
+        usesAtUseLoc = [u | u <- tm.uses, useLoc == u.occ];
+        defsAtDefLoc = [d | d <- tm.defines, defLoc == d.defined];
+        reachable = (u: scopeGraph.lookup(u) | u <- usesAtUseLoc);
+        if (u <- usesAtUseLoc, d <- defsAtDefLoc, d.defined in reachable[u]) {
+
+            assert u.id == d.id :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have equal `id` fields. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.id>` (`u.id`) isn\'t equal to `<d.id>` (`d.id`).";
+
+            assert u.orgId == d.orgId :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have equal `orgId` fields. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.orgId>` (`u.orgId`) isn\'t equal to `<d.orgId>` (`d.orgId`).";
+
+            assert d.idRole in u.idRoles :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have compatible roles. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.idRoles>` (`u.idRoles`) doesn\'t contain `<d.idRole>` (`d.idRole`).";
+
+        } else {
+
+            assert false : 
+                "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, `defLoc` is reachable from `useLoc` in the scope graph. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<defLoc>` (`defLoc`) isn\'t reachable from `<useLoc>` (`useLoc`), but `<reachable>` are.";
+        }
+    }
+}
+
 // Implementation of the Solver data type: a collection of call backs
 
 Solver newSolver(Tree pt, TModel tm){
@@ -1735,6 +1792,9 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         //println("definedBy;"); iprintln(definedBy);
         tm.useDef = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
 
+        // Update `uses` with all uses resolved by the solver
+        tm.uses = [*({*tm.uses} + {*def2uses[d] | d <- def2uses})];
+
         ldefines = for(tup: <loc _, str _, str _, IdRole _, loc defined, DefInfo defInfo> <- tm.defines){
                         if(defInfo has tree){
                             l = getLogicalLoc(defInfo.tree);
@@ -1765,7 +1825,8 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         messages =  visit(messages) { case loc l => solver_toPhysicalLoc(l) };
         tm.messages = sortMostPrecise(toList(toSet(messages)));
 
-        checkAllTypesAvailable(tm);
+        assertValidDefines(tm);
+        assertValidUseDef(tm, thisSolver);
         return tm;
     }
 

src/analysis/typepal/TestFramework.rsc

@@ -73,7 +73,7 @@ bool matches(str subject, str pat){
 str spinChar(int n)
     = n < 0 ? "|" : (0: "|", 1: "/", 2: "-", 3: "\\")[n%4];
 
-bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, bool verbose = false, set[str] runOnly = {}, str runName = ""){
+bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t, str name) getModel, bool verbose = false, set[str] runOnly = {}, str runName = ""){
     TTL ttlProgram = [TTL] "";
 
     map[tuple[str, loc], list[Message]]failedTests = ();
@@ -100,12 +100,14 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
                 continue;
             }
             ntests += 1;
+            newTreeSrc = |unknown:///|;
             try {
               newTree = visit(parse(begin, "<ti.tokens>")) {
                 case Tree t => t[src = relocate(t.src, ti.tokens.src)]
                     when t has src
               };
-              model = getModel(newTree);
+              newTreeSrc = newTree.src;
+              model = getModel(newTree, "<ti.name>");
               list[Message] messages = model.messages;
               if(verbose) println("runTests: <messages>");
               expected = ti.expect is none ? {} : {deescape("<s>"[1..-1]) | TTL_String s <- ti.expect.messages};
@@ -118,7 +120,9 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
                 failedTests[<"<ti.name>", suite>]  = [error("Parse error", relocate(l, ti.tokens.src))];
            } catch Ambiguity(loc l, nt, inp): {
                 failedTests[<"<ti.name>", suite>]  = [error("Ambiguity (<nt> on `<inp>`)", (l.offset?) ? relocate(l, ti.tokens.src) : l)];
-           } 
+           } catch AssertionFailed(str s): {
+                failedTests[<"<ti.name>", suite>]  = [error("Assertion failed: <s>", newTreeSrc)];
+           }
 
         }
         testTime += (cpuTime() - startTests);
@@ -143,7 +147,7 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
         }
     }
     println("Parse time: <parseTime/1000000> msec; Test time: <testTime/1000000> msec");
-    return ok;
+    return ok && isEmpty(failedTests);
 }
 
 lrel[&T<:Tree, set[str]] extractTests(list[loc] suites, type[&T<:Tree] begin) {

src/examples/aliases/Test.rsc

@@ -20,8 +20,8 @@ import ParseTree;
 
 // ---- Testing ---------------------------------------------------------------
 
-TModel aliasesTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = aliasesConfig(), modelName = "alias");
+TModel aliasesTModelForTree(Tree pt, bool assertValidUseDef = true){
+    return collectAndSolve(pt, config = aliasesConfig()[assertValidDefines = true][assertValidUseDef = assertValidUseDef], modelName = "alias");
 }
 
 TModel aliasesTModelFromName(str mname){
@@ -32,7 +32,10 @@ TModel aliasesTModelFromName(str mname){
 test bool aliasesTests() {
     return runTests([|project://typepal/src/examples/aliases/aliases.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return aliasesTModelForTree(t); },
+                    // Enable `assertValidUseDef` only when the program under
+                    // test **isn't** `CircularAlias1` (which is expected to
+                    // have an invalid `useDef`).
+                    TModel (Tree t, str name) { return aliasesTModelForTree(t, assertValidUseDef = name != "CircularAlias1"); },
                     runName = "Aliases");
 }
 

src/examples/calc/Test.rsc

@@ -21,7 +21,7 @@ import ParseTree;                           // In order to parse tests
 // ---- Testing ---------------------------------------------------------------
 
 TModel calcTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName = "calc");
+    return collectAndSolve(pt, modelName = "calc", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel calcTModelFromStr(str text){
@@ -32,7 +32,7 @@ TModel calcTModelFromStr(str text){
 test bool calcTests() {
      return runTests([|project://typepal/src/examples/calc/tests.ttl|], 
                      #Calc, 
-                     calcTModelForTree, 
+                     TModel (Tree t, str _name) { return calcTModelForTree(t); },
                      runName="Calc");
 }
 

src/examples/dataModel/Test.rsc

@@ -17,7 +17,7 @@ extend examples::dataModel::Checker;
 extend analysis::typepal::TestFramework;
 
 TModel dmTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = dmConfig());
+    return collectAndSolve(pt, config = dmConfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel dmTModelFromName(str mname){

src/examples/evenOdd/Test.rsc

@@ -23,7 +23,7 @@ import ParseTree;                           // In order to parse tests
 
 TModel evenOddTModelForTree(Tree pt){
     if(pt has top) pt = pt.top;
-    c = newCollector("even-odd", pt,  tconfig());
+    c = newCollector("even-odd", pt, tconfig()[assertValidDefines = true][assertValidUseDef = true]);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
 }
@@ -36,7 +36,7 @@ TModel evenOddTModelFromStr(str text){
 test bool evenOddTests() {
      return runTests([|project://typepal/src/examples/evenOdd/tests.ttl|], 
                      #EvenOdd, 
-                     evenOddTModelForTree, 
+                     TModel (Tree t, str _name) { return evenOddTModelForTree(t); },
                      runName="EvenOdd");
 }
 

src/examples/fixedMembers/Test.rsc

@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel fixedMembersTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = fixedMembersConfig(), modelName="fixed-members");
+    return collectAndSolve(pt, config = fixedMembersConfig()[assertValidDefines = true][assertValidUseDef = true], modelName = "fixed-members");
 }
 
 TModel fixedMembersTModelFromName(str mname){
@@ -33,7 +33,7 @@ TModel fixedMembersTModelFromName(str mname){
 test bool fixedMembersTests() {
     return runTests([|project://typepal/src/examples/fixedMembers/fixedMembers.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return fixedMembersTModelForTree(t); },
+                    TModel (Tree t, str _name) { return fixedMembersTModelForTree(t); },
                     runName = "fixedMembers");
 }
 

src/examples/fun/Test.rsc

@@ -27,7 +27,7 @@ TModel funTModel(str name){
 }
 
 TModel funTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName = "fun");
+    return collectAndSolve(pt, modelName = "fun", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel funTModelFromStr(str text){
@@ -41,6 +41,12 @@ list[Message] funCheck(str name) {
 }
 
 test bool funTests() 
-    =  runTests([|project://typepal/src/examples/fun/tests.ttl|], #Fun, funTModelForTree, runName="Fun");
+    = runTests([|project://typepal/src/examples/fun/tests.ttl|],
+                #Fun,
+                TModel (Tree t, str _name) { return funTModelForTree(t); },
+                runName="Fun");
+
+test bool funTModelTestBig() = [] := funTModel("big").messages;
+test bool funTModelTestTmp() = [] := funTModel("tmp").messages;
 
 value main() = funTests();

src/examples/fwjava/Test.rsc

@@ -23,7 +23,7 @@ import ParseTree;
 TModel fwjTModelForTree(Tree pt){
     if(pt has top) pt = pt.top;
 
-    c = newCollector("fwj", pt, fwjConfig());
+    c = newCollector("fwj", pt, fwjConfig()[assertValidDefines = true][assertValidUseDef = true]);
     fwjPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -37,8 +37,18 @@ TModel fwjTModelFromName(str mname, bool _){
 test bool fwjTests() {
     return runTests([|project://typepal/src/examples/fwjava/tests.ttl|], 
                      #start[FWJProgram], 
-                     TModel (Tree t) { return fwjTModelForTree(t); },
+                     TModel (Tree t, str _name) { return fwjTModelForTree(t); },
                      runName = "FwJava");
 }
 
+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);
+    return true;
+}
+
 value main() = fwjTests();

src/examples/modfun/A.mfun

@@ -2,4 +2,4 @@ module A {
     import B;
     def a : int -> int = fun i : int { 5 + i };
     def a : int -> int = fun i : int { 6 + i };
-}
+}

src/examples/modfun/Test.rsc

@@ -28,7 +28,7 @@ TModel modfunTModel(str name){
 }
 
 TModel modfunTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName="modfun");
+    return collectAndSolve(pt, modelName="modfun", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 TModel modfunTModelFromStr(str text){
@@ -43,9 +43,13 @@ list[Message] modfunCheck(str name) {
 
 test bool modfunTests()
     = runTests([|project://typepal/src/examples/modfun/tests.ttl|], 
-               #ModFun,
-               modfunTModelForTree,
-               runName = "ModFun");
+                #ModFun,
+                TModel (Tree t, str _name) { return modfunTModelForTree(t); },
+                runName = "ModFun");
+
+test bool modfunTModelTestA() = [_, _, _] := modfunTModel("A").messages; // Three errors expected
+test bool modfunTModelTestB() = [_, _] := modfunTModel("B").messages; // Two errors expected
+test bool modfunTModelTestTmp() = [] := modfunTModel("tmp").messages;
 
 value main() 
     =  modfunTests();

src/examples/modules/Checker.rsc

@@ -147,7 +147,7 @@ list[Message] runModules(str name, bool debug = false) {
 }
 
 bool testModules(int n, bool debug = false, set[str] runOnly = {}) {
-    return runTests([|project://modules-core/src/lang/modules/modules<"<n>">.ttl|], #start[Program], TModel (Tree t) {
+    return runTests([|project://modules-core/src/lang/modules/modules<"<n>">.ttl|], #start[Program], TModel (Tree t, str _name) {
         return modulesTModelFromTree(t);
     }, runOnly = runOnly);
 }

src/examples/pascal/Test.rsc

@@ -26,7 +26,7 @@ import util::Reflective;
 TModel pascalTModelForTree(Tree pt, str programName, PathConfig _, bool _){
     if(pt has top) pt = pt.top;
 
-    c = newCollector(programName, pt, pascalConfig());
+    c = newCollector(programName, pt, pascalConfig()[assertValidDefines = true][assertValidUseDef = true]);
     pascalPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -35,7 +35,7 @@ TModel pascalTModelForTree(Tree pt, str programName, PathConfig _, bool _){
 TModel pascalTModelForTree(Tree pt, bool _){
     if(pt has top) pt = pt.top;
 
-    c = newCollector("pascal", pt, pascalConfig());
+    c = newCollector("pascal", pt, pascalConfig()[assertValidDefines = true][assertValidUseDef = true]);
     pascalPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -57,7 +57,7 @@ test bool pascalTests() {
     //return true;
     bool ok = runTests([|project://typepal/src/examples/pascal/expression-tests.ttl|,
                         |project://typepal/src/examples/pascal/statement-tests.ttl|
-                       ], #start[Program], TModel (Tree t) { return pascalTModelForTree(t, false); },
+                       ], #start[Program], TModel (Tree t, str _name) { return pascalTModelForTree(t, false); },
                        runName = "Pascal");
     println("Executing Pascal examples\r");
     int n = 0;

src/examples/pico/Test.rsc

@@ -22,19 +22,21 @@ import ParseTree;
 
 TModel picoTModelFromName(str name) {
     Tree pt = parse(#start[Program], |project://typepal/src/examples/pico/<name>.pico|);
-    return collectAndSolve(pt, modelName="pico");
+    return collectAndSolve(pt, modelName="pico", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 TModel picoTModelForTree(Tree pt) {
-    return collectAndSolve(pt, modelName="pico");
+    return collectAndSolve(pt, modelName="pico", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 test bool picoTests() {
     return runTests([|project://typepal/src/examples/pico/tests.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return picoTModelForTree(t); },
+                    TModel (Tree t, str _name) { return picoTModelForTree(t); },
                     runName = "Pico");
 }
 
+test bool picoTModelTestFac() = [] := picoTModelFromName("fac").messages;
+
 value main()
     = picoTests();