NPE when launching a SMT-DSE without allocation constraints (WKIA model)
Observed Exception
!ENTRY org.fortiss.af3.exploration 4 4 2019-09-08 13:46:20.150
!MESSAGE Error executing DSE:
null.
!STACK 0
java.lang.NullPointerException
at com.microsoft.z3.Context.checkContextMatch(Context.java:3974)
at com.microsoft.z3.Context.mkFuncDecl(Context.java:480)
at
com.microsoft.z3.Z3javaAPIWrapper.createFunction(Z3javaAPIWrapper.java:98)
at
org.fortiss.af3.exploration.smt.modeltransformation.DSMLTransformationService.getAllocateFunction(DSMLTransformationService.java:499)
at
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.createAllocationExpression(DefaultExpressionTransformator.java:311)
at
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.createLocationExpression(DefaultExpressionTransformator.java:221)
at
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.toSMTBoolean(DefaultExpressionTransformator.java:171)
at
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.transform(DefaultExpressionTransformator.java:107)
at
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
at
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.toQuantifier(NonQuantifiedExpressionTransformator.java:80)
at
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.transform(NonQuantifiedExpressionTransformator.java:62)
at
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
at
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.toQuantifier(NonQuantifiedExpressionTransformator.java:80)
at
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.transform(NonQuantifiedExpressionTransformator.java:62)
at
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
at
org.fortiss.af3.exploration.smt.modeltransformation.DSMLtoSMTTransformator.extractSMTExpr(DSMLtoSMTTransformator.java:262)
at
org.fortiss.af3.exploration.smt.modeltransformation.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:187)
at
org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solve(SolverRun.java:188)
at
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:163)
at
org.fortiss.af3.exploration.service.internal.DSEBackendService$1.run(DSEBackendService.java:174)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.150
!MESSAGE com.microsoft.z3.Context.checkContextMatch(Context.java:3974)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE com.microsoft.z3.Context.mkFuncDecl(Context.java:480)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
com.microsoft.z3.Z3javaAPIWrapper.createFunction(Z3javaAPIWrapper.java:98)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DSMLTransformationService.getAllocateFunction(DSMLTransformationService.java:499)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.createAllocationExpression(DefaultExpressionTransformator.java:311)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.createLocationExpression(DefaultExpressionTransformator.java:221)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.toSMTBoolean(DefaultExpressionTransformator.java:171)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DefaultExpressionTransformator.transform(DefaultExpressionTransformator.java:107)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.151
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.toQuantifier(NonQuantifiedExpressionTransformator.java:80)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.transform(NonQuantifiedExpressionTransformator.java:62)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.toQuantifier(NonQuantifiedExpressionTransformator.java:80)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.NonQuantifiedExpressionTransformator.transform(NonQuantifiedExpressionTransformator.java:62)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.ConstraintTransformationAdapter.transform(ConstraintTransformationAdapter.java:97)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DSMLtoSMTTransformator.extractSMTExpr(DSMLtoSMTTransformator.java:262)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.DSMLtoSMTTransformator.transform(DSMLtoSMTTransformator.java:187)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.modeltransformation.SolverRun.solve(SolverRun.java:188)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:163)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.152
!MESSAGE
org.fortiss.af3.exploration.service.internal.DSEBackendService$1.run(DSEBackendService.java:174)
!SUBENTRY 1 org.fortiss.af3.exploration 4 0 2019-09-08 13:46:20.153
!MESSAGE org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Background
This error occurs since the BasicDeploymentConstraints are not generated first. Please find a mechanism to avoid this kind of errors (maybe some automatic detection in the DSEML transformator) since this is the third or fourth time in a year that this bug reoccurs. Manually managing the order in which the constraints are generated in the Z3Backend does not seem to be a scalable solution.
Steps to reproduce
- Load the WIKA model.
- Import it into the DSE perspective.
- DO NOT create any constraints.
- Go to Deployment >Generate and observe the exception.
(from redmine: issue id 3814, created on 2019-09-08, closed on 2019-10-01)