szabta89 / inca Goto Github PK

View Code? Open in Web Editor NEW

86.0 86.0 6.0 112.99 MB

Incremental Program Analysis Framework

License: Eclipse Public License 2.0

Xtend 96.00% Java 4.00%

analysis-framework domain-specific-language dsl incremental-computation language-workbench mps program-analysis

inca's People

Contributors

Stargazers

Watchers

Forkers

sander2 chubbymaggie seba-- tiandiyixian unshorn ilya-klyuchnikov

inca's Issues

incorrect analysis result

I think I found another bug. I have two functions, f1 and f2. I expect these to behave identically, but they do not. While f2 works as expected, f1 does not yield any tuples, even though g1 returns no tuples where the first argument is a Lifetime.

join type LifetimeRelated = Lifetime | LifetimeDefinition                                                                                                                     
                                                                                                                                                                              
def g1(from : LifetimeRelated, l : Lifetime) : Void = { 
  assert from instanceOf LifetimeDefinition 
  lifetimeNode := from.lifetime 
  assert lifetimeNode.name == l.name 
}
                                                                                                                                                                              
private def f1(l : Lifetime) : Void = { 
  assert undef g1(l, l) 
}                                                                                                           
private def f2(l : Lifetime) : Void = { 
  assert def f2_helper(l, l) 
}                                                                                                      
private def f2_helper(l1 : Lifetime, l2 : Lifetime) : Void = { 
  assert undef g1(l1, l2) 
}                                                                                  
                                                                                                                                                                              
// unused fucntion, added to see how it compiles                                                                                                                              
private def h1(s : LifetimeDefinition) : Void = { 
  bla := s.lifetime 
}

The code I'm analyzing is struct Y1 < 'a > { } and the result is (notice the difference between f1 and f2):

Typing.g1 (1)
    "from"=LifetimeDefinition, "l"='a
Typing.f1 (0)
Typing.f2 (1)
    "l"='a
Typing.f2_helper (1)
    "l1"='a, "l2"='a

Even though g1 returns the correct tuples, I found its transformed code to be suspicious:

Note that lifetime is looked up in BaseConcept, whereas in h1 it's (correctly) looked up in LifetimeDefinition. I'm not sure how that would cause f1 to misbehave, but I thought I'd mention it anyway.

I pushed the example to my repo under the same-var-bug branch.

switch causing error

This code causes an error type y8 is not a subtype of (node<>, node<FunctionArg>), located on the first alternative of getUniqueInputLifetimes1:

join type LifetimeDeclarator = Lifetime | PointerType
                                                     
private def getUniqueInputLifetimes1(f : Function) : (LifetimeDeclarator, FunctionArg) = { 
  arg := f.args 
  ty := arg.ty 
  q := typeGetUsedPointerTypes(ty) 
  switch { 
    assert undef q.lifetime 
    return (q, arg) 
  } alt { 
    lifetime := q.lifetime 
    decl := resolveLifetime(lifetime, lifetime) 
    return (decl, arg) 
  } 
}

Even though the manually desugared version works just fine:

private def getUniqueInputLifetimes2(f : Function) : (LifetimeDeclarator, FunctionArg) = { 
  arg := f.args 
  ty := arg.ty 
  q := typeGetUsedPointerTypes(ty) 
  assert undef q.lifetime 
  return (q, arg) 
} alt { 
  arg := f.args 
  ty := arg.ty 
  q := typeGetUsedPointerTypes(ty) 
  lifetime := q.lifetime 
  decl := resolveLifetime(lifetime, lifetime) 
  return (decl, arg) 
}

(code pushed to my switch-error branch)

slow computation network construction

Building the computation network takes a long time for complicated analyses (this should be reported to Viatra at some point); in my case, it takes about 10-15s. This initialization seems to be separately for each model that is analyzed. As a result, my test suite, which analyzed three different models, spent a lot of time recomputing the computation network. For now, I have merged all my three (test program) models to greatly speedup testing time.

unexpected behavior in `assert undef a.b.c`

These two snippets behave differently when a.b is defined, but a.b.c is not:

assert undef a.b.c

and

tmp := a.b
assert undef tmp.c

Ideally, assert undef a.b.c should be equivalent to:

switch{
    assert undef a.b
} alt {
    tmp := a.b
    assert undef tmp.c
}

If that's not possible, then only using the second part of the switch would be acceptable. If that's not possible either, then a compiler error should be thrown when this construct is used.

Type checking bug for return type

Actual behavior
A function with an empty body like the one below passes the type checker and happily compiles, even though it lacks a return statement. It will simply return all nodes of type Expr that are in the model.

private def f(f : Function) : Expr = { 
   
}

Expected behavior
The type checker should mark the function as invalid, like it does when there is any statement inside the body and the return type is incorrect. For example, the function below correctly detects a type error:

private def g(f : Function) : Expr = { 
    // useless assertion to make type checker work
   assert x instanceOf Expr
}

Reproduction
See this branch, with this analysis function and this analysis target.

Error while editing code

I received the following error while editing IncA code:

java.lang.AssertionError: You can't edit unregistered node
	at jetbrains.mps.ide.editor.MPSEditorOpener.doOpenNode(MPSEditorOpener.java:81)
	at jetbrains.mps.ide.editor.MPSEditorOpener.openNode(MPSEditorOpener.java:77)
	at jetbrains.mps.ide.navigation.NavigationSupportImpl.openNode(NavigationSupportImpl.java:54)
	at org.inca.ui.plugin.MouseListener$1.run(MouseListener.java:63)
	at jetbrains.mps.smodel.ActionDispatcher.dispatch(ActionDispatcher.java:84)
	at jetbrains.mps.smodel.ActionDispatcher.lambda$wrap$0(ActionDispatcher.java:105)
	at jetbrains.mps.smodel.LockRunnable.run(LockRunnable.java:60)
	at com.intellij.openapi.application.impl.ApplicationImpl.runWriteAction(ApplicationImpl.java:1057)
	at jetbrains.mps.smodel.TryRunPlatformWriteHelper.runWrite(TryRunPlatformWriteHelper.java:103)
	at jetbrains.mps.smodel.WorkbenchModelAccess.runWriteAction(WorkbenchModelAccess.java:98)
	at jetbrains.mps.smodel.ModelAccessBase.runWriteAction(ModelAccessBase.java:64)
	at org.inca.ui.plugin.MouseListener.mousePressed(MouseListener.java:61)
	at java.awt.AWTEventMulticaster.mousePressed(AWTEventMulticaster.java:280)
	at java.awt.Component.processMouseEvent(Component.java:6545)
	at javax.swing.JComponent.processMouseEvent(JComponent.java:3325)
	at java.awt.Component.processEvent(Component.java:6313)
	at java.awt.Container.processEvent(Container.java:2237)
	at java.awt.Component.dispatchEventImpl(Component.java:4903)
	at java.awt.Container.dispatchEventImpl(Container.java:2295)
	at java.awt.Component.dispatchEvent(Component.java:4725)
	at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4889)
	at java.awt.LightweightDispatcher.processMouseEvent(Container.java:4523)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:4467)
	at java.awt.Container.dispatchEventImpl(Container.java:2281)
	at java.awt.Window.dispatchEventImpl(Window.java:2746)
	at java.awt.Component.dispatchEvent(Component.java:4725)
	at java.awt.EventQueue.dispatchEventImpl(EventQueue.java:764)
	at java.awt.EventQueue.access$500(EventQueue.java:98)
	at java.awt.EventQueue$3.run(EventQueue.java:715)
	at java.awt.EventQueue$3.run(EventQueue.java:709)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:90)
	at java.awt.EventQueue$4.run(EventQueue.java:737)
	at java.awt.EventQueue$4.run(EventQueue.java:735)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:734)
	at com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:719)
	at com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:664)
	at com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:363)
	at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:201)
	at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:82)

Match statement in lattices cannot be nested

A match statement inside another match statement will give a compilation error, since duplicate variables case_0 will be generated.

Editor errors are ignored

When there are errors in a pattern function module, IncA should refuse to compile, but the current behavior is that it will happily compile and run the analysis.

Differential data-flow evaluation in the backend

This is a research endeavour. The idea is to create an alternative evaluation strategy in the RETE network that is based on differential dataflow. The technique is best described in "Differential Dataflow - F McSherry, DG Murray, R Isaacs, M Isard - CIDR, 2013".

This issue is also tracked on the Viatra Queries issue tracker https://bugs.eclipse.org/bugs/show_bug.cgi?id=543400.

IDE cpu usage

I pushed some code to slow-ide2, which, when the test is run, generates about 10000 lines worth of error messages. When the test is done and when the first result is single-clicked (i.e. test_core), CPU usage goes to 100% for about a minute (even though the editor remains responsive). I believe this is caused by some highlighter functionality in MPS (AsyncFilterRunner.runTasks).

Edit: I think it may be converting references to code (such as TypeLattice.java:847) into clickable links.

Universal quantification

It happens quite often that you need to assert that a function is defined for all items in some list (or set of tuples). There are ways to implement this in IncA, but they each have their drawbacks.

Through recursion

def containerOk(c: Container) {
  e := c.elems
  assert undef e.prev
  assert def checkElemListRecursively(e)
} alt {
  assert undef c.elems
}
def checkElemListRecursively(e: Elem) {
  // omitted: assert that e is valid

  switch {
    assert undef e.next
  } alt {
    assert def checkElemListRecursively(e.next)
  }
}

This is not very nice to write and the recursive nature likely has a negative impact on the performance. Also, it only works on lists and not on a set a values returned by a function.

Through negation

def containerOk(c: Container) {
  assert undef containerElemNok(c)
}
def containerElemNok(c: Container) {
  e := c.elems
  // omitted: assert that e is invalid
}

This has the downside that it uses undef, which in some situations can lead to negation in recursion. On the upside, there is less boilerplate required than the other solutions.

Through lattice aggregation

def containerOk(c: Container) {
  assert containerElemOk(c) == BoolLattice.True
}
def containerElemOk(c: Container) : BoolLattice/intersection {
  e := c.elems
  
  switch {
    assert def elemOk(e)
    return BoolLattice.True 
  } alt {
    assert undef elemOk(e)
    return BoolLattice.False
  }
} alt {
  assert undef c.elems
  return BoolLatice.True
}
def elemOk(e: Elem) {
    // omitted: assert that e is valid
}

Like the previous solution, this has the downside that an undef is required (in the second alternative of the switch). Also, it's a bit verbose. However, its performance is likely better than the recursive solution.

Ideal solution

Some kind of support for universal quantification. Something like the example below would be ideal.

def containerOk(c: Container) {
  // universal quantification on a list:
  foreach e in c.elems {
    // omitted: assert that e is valid
  }
  // it would be even better if it would also work on the result of a function call:
  foreach e in getAllElems(c) {
    // omitted: assert that e is valid
  }
}

Implementation

It's probably fairly easy to transform the suggested syntax into code as shown in case 2 or 3. That would, however, introduce assert undefs. Could these be avoided somehow?

[low priority feature request] IncA Explorer node labels

In my AST I often have a lot of nodes of type Path. These paths do not implement INamedConcept, so in the IncA explorer, these simply show up as Path. It would be great if there were some way to override the name displayed in the explorer, such that I don't have to double click on every single Path to find the one I'm looking for.

Compilation time: debug option

(as discussed)

As my project grows, the time spent in the hints optimizer is getting quite annoying again, even when most functions are marked as private. The hints optimizer can be disabled at IncA compile time using the IncARuntimeOptions.useHintGuidedCaching flag, but it would be great if the optimizer could be switched on and off from within MPS without requiring an IncA recompilation.

Input parameters should not have lattice type

There should be an error reporting about this issue because this is probably an immediate violation of functional dependency.

Binding generated data

Using strings that are generated by Java code are handled incorrectly. This works:

assert MyLattice.randomString() == "test"

But this does not:

x := MyLattice.randomString()
assert x == "test"

You explained that generated data can never be returned from a pattern function, but that it should be allowed to be bound to temporary variables. However, during compilation, the code is transformed in such a way that all variables are returned as part of a generated function. Thus, the transformed code is illegal and does not work.

The type com.mbeddr.mpsutil.inca.core.runtime.plugin.MPSQuerySpecificationHints cannot be resolved.

Rebuild fails for this IncA project: Experiment1/TestPCFnew in https://github.com/seba--/inca-experiments/tree/import-failure

Error stack:

[jetbrains.mps.make.ModuleMaker] Cycle #1: [[Experiment1 [solution]]]
[jetbrains.mps.make.CompilationErrorsHandler@5a580b5d] Compilation problems
[jetbrains.mps.make.CompilationErrorsHandler@5a580b5d] Modules: [Experiment1 [solution]];
Classpath: classpath {
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/capsule-0.4.0-20170621.132553-7.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.emf.common_2.13.0.v20170609-0707.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/platform.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/ecj-4.7.2.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/languageDesign/jetbrains.mps.lang.smodel.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/util.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/extensions.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.osgi_3.12.50.v20170928-1321.jar
	file-cp: /Users/seba/projects/inca/code/languages/org.inca.core/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-closures.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-editor.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.data.runtime/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/languageDesign/jetbrains.mps.lang.traceable.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-messaging.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/languageDesign/jetbrains.mps.lang.core.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/platform-impl.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/baseLanguage/jetbrains.mps.baseLanguage.scopes.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-annotations.jar
	file-cp: /Users/seba/projects/inca-experiments/solutions/Experiment1/classes_gen
	file-cp: /Users/seba/projects/inca-experiments/languages/PCF/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/baseLanguage/jetbrains.mps.baseLanguage.collections.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime.matchers_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/jre/jdk/Contents/Home/jre/lib/charsets.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.gp.runtime/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-collections.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/jre/jdk/Contents/Home/jre/lib/ext/jfxrt.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/asm-all.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-platform.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime.base_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-openapi.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime.rete.recipes_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/languageDesign/jetbrains.mps.lang.structure.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime.base.itc_2.0.0.2018.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.hints/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-core.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.emf.ecore_2.13.0.v20170609-0707.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-editor-api.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.xtext.xbase.lib_2.12.0.v20170518-0757.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-behavior-api.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.core.runtime_3.13.0.v20170207-1030.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/openapi.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.emf.codegen.ecore_2.13.0.v20170609-0928.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/netty-all-4.1.13.Final.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/jre/jdk/Contents/Home/jre/lib/rt.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/jre/jdk/Contents/Home/jre/lib/jsse.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/languageDesign/jetbrains.mps.lang.modelapi.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/jre/jdk/Contents/Home/jre/lib/jce.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.fun.runtime/classes_gen
	file-cp: /Users/seba/projects/inca-experiments/languages/FeatherweightJava/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/baseLanguage/jetbrains.mps.baseLanguage.closures.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/commons-imaging-1.0-RC.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/jdom.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/xstream-1.4.8.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/guava-21.0.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/picocontainer.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.collections_9.0.0.v20170920-0536.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-tuples.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/annotations.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-editor-runtime.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.transformation.evm_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-behavior-runtime.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-logging.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/log4j.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.xtext.xbase_2.12.0.v20170519-0752.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.core.databinding.observable_1.6.100.v20170515-1119.jar
	jar-cp: /Users/seba/projects/inca/artifacts/com.mbeddr.platform/com.mbeddr.mpsutil.common/languages/group.common/com.mbeddr.mpsutil.common.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/baseLanguage/jetbrains.mps.baseLanguage.javadoc.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-boot-util.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.addon.databinding.runtime_2.0.0.2018.jar
	file-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.util/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/trove4j.jar
	file-cp: /Users/seba/projects/inca-experiments/solutions/FeatherweightJavaImporter/classes_gen
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/mps-icons.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.viatra.query.runtime.rete_2.0.0.2018.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/platform-api.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/languages/baseLanguage/jetbrains.mps.baseLanguage.jar
	jar-cp: /Applications/MPS 2018.1.app/Contents/lib/forms_rt.jar
	jar-cp: /Users/seba/projects/inca/code/solutions/org.inca.core.runtime/lib/org.eclipse.equinox.common_3.9.0.v20170207-1454.jar
}

[jetbrains.mps.make.CompilationErrorsHandler@5a580b5d] TestPCF/BottomUp_TypeOfReference_WrappedQuerySpecification.java : The type com.mbeddr.mpsutil.inca.core.runtime.plugin.MPSQuerySpecificationHints cannot be resolved. It is indirectly referenced from required .class files (line: 1)
[jetbrains.mps.make.CompilationErrorsHandler@5a580b5d] 

TestPCF/BottomUp_TypeOfReference_WrappedQuerySpecification.java : The import com.mbeddr.mpsutil.inca cannot be resolved (line: 5)
TestPCF/BottomUp_TypeOfReference_WrappedQuerySpecification.java : The import com.mbeddr.mpsutil.inca cannot be resolved (line: 6)
TestPCF/BottomUp_TypeOfReference_WrappedQuerySpecification.java : The import com.mbeddr.mpsutil.inca cannot be resolved (line: 10)
... (goes on like that)

how to run and update analyses

I've successfully built IncA and configured MPS. I also saw the IncA explorer plugin which brings up some panels that says "program analyses", "subject programs" and shows 4 buttons. However I couldn't figure out how to run analyses - what is the user supposed to do here?

Type checking error

This function works:

private def fieldsVariantHasDuplicateNames(v : FieldsVariant) : Void = { 
  x := v.fields 
  y := v.fields 
  assert x.name == y.name 
  assert x != y 
}

... but this does not:


private def fieldsVariantHasDuplicateNames(v : FieldsVariant) : Void = { 
  x := v.fields 
  y := v.fields 
  assert x != y 
  assert x.name == y.name 
}

In the last version, x.name and y.name can not be resolved, since assert x != y removes typing information in x and y.

Code to reproduce the problem pushed to my type-checking-error branch.

Allow cyclic imports among IncA modules

The backend can already handle cyclic imports, so far, we disallowed them on the DSL level. Allowing cyclic imports helps to break up large analysis modules. We should still issue an "info" in the presence of cycles.

return from within match

Return statements in pattern matches in lattice code don't work as I'd expect them to. This works:

def lookupField(s : TypeLattice, fieldName : string) : TypeLattice = {
    TypeLattice ret = Invalid;
    match s with {
        case StructType(structName, fields) => {
            if (fields.containsKey(fieldName)) {
                ret = fields[fieldName];
            }
        }
    };
    return ret;
}

but this doesn't:

def lookupField(s : TypeLattice, fieldName : string) : TypeLattice = {
    match s with {
        case StructType(structName, fields) => {
            if (fields.containsKey(fieldName)) { return fields[fieldName]; }
        }
    };
    return Invalid;
}

I think that since match is compiled into an anonymous function, a return inside match actually assigns the value to result of the match expression, rather than to the result of the function. This might be intended behavior, but if so, it should probably be documented somewhere

Name shadowing in match

This code:

def toTypeRefs(t : TypeLattice) : TypeLattice = { 
  match t with { 
    case StructType(n, f1) => return TypeRef(n); 
    case Pointer(mut, t) => return Pointer(mut, toTypeRefs(t)); 
    case _ => return t; 
  }; 
}

generates this code:

public TypeLattice.TypeLatticeElement toTypeRefs(TypeLattice.TypeLatticeElement t) {
    {
      final Object[] values = {t};

     // declare the local variables for the case matchers 
      Map<String, Object> case_0;
      Map<String, Object> case_1;
      Map<String, Object> case_2;

     if ((case_0 = new SequenceMatcher(matcher_a0a0k).match(values)) != null) {
        Map<String, TypeLattice.TypeLatticeElement> f1 = (Map<String, TypeLattice.TypeLatticeElement>) case_0.get("f1");
        String n = (String) case_0.get("n");
        return TypeLattice.TypeRef.create(n);
      } else if ((case_1 = new SequenceMatcher(matcher_a1a0k).match(values)) != null) {
        TypeLattice.TypeLatticeElement t = (TypeLattice.TypeLatticeElement) case_1.get("t");
        boolean mut = (boolean) case_1.get("mut");
        return TypeLattice.Pointer.create(mut, TypeLattice.instance().toTypeRefs(t));
      } else if ((case_2 = new SequenceMatcher(WildCardMatcher.INSTANCE).match(values)) != null) {
        return t;
      } else {
        throw new PatternMatcherException(values);
      }
    }
  }

which redeclares t in the first else if.

Either (1) an error should be shown in the editor, or (2) the generator should generate a new name. Option 1 would probably be more consistent with the rest of Java; args and locals can not usually be shadowed in Java.

investigate how to introduce inline functions

For code organization purposes, it often makes sense to build up the analysis from smaller analysis functions. However, the small pieces may introduce a large number of tuples because of potential cross product among the parameters. It would make sense to mark function as inline, so that at runtime the constraints of the function would be inlined into the caller.

Use IncA as a test suite for VIATRA Query runtime

The complex recursive queries provided by IncA would be a good candidate for testing the VIATRA Query runtime for regressions. For this to work, the following steps are necessary:

Gradle should load VIATRA query plug-ins from a maven repository (like https://repo.eclipse.org/content/groups/viatra/)
For easier debugging, there should be an alternative pull in the VIATRA jars as local dependencies, e.g. jars or Eclipse projects
Include the inter-procedural points-to analysis in the test suite.
Set up a build job that executes these tests in a location that is visible to VIATRA committers, if possible on ci.eclipse.org; or if necessary at a build server provided by IncQuery Labs

I try to help with the related issues as I have time (most likely in January).

Add support for algebraic data types

Compared to lattices, they don't need aggregation operators. The engine should simply collect ADT values.