This project is read-only.
1

Closed

XML Exporting throws a null pointer exception

description

This happens in two cases:

1) when there is a case distinction, the other case is denoted by null

see for example: text-model/parsing/test206.tla

2) when there is an instantiation of another module containing a parametrized theorem:
if instantiating a module fails because the substitution leads to an incorrect program(in this xase to x''), the semantic tree contains a null reference

see for example: test-models/parsing/test217.tla
Closed Oct 7, 2016 at 5:10 PM by mku

comments

libal wrote Dec 31, 2014 at 7:05 PM

1)

given module:
EXTENDS Integers

df(x) == CASE x < 0 -> -1
       [] x = 0 -> 0
       [] OTHER -> 1  
debugging using the explorer:
tlaplus/tlatools/dist$ java -cp tla2tools.jar tla2sany.SANY -d ~/Documents/tla/repository/trunk/v2-tlapm/Toy.tla

gives:
*OpDefNode: df
uid: 255  kind: UserDefinedOpKind  arity: 1  orgDefInModule: Toy
local: false
letInLevel: 0
inRecursive: false
inRecursiveSection: false
recursiveSection: -1
local: false
source: this
originallyDefinedInModule: Toy (uid: 239)
Formal params: 1
| | *FormalParamNode: x uid: 240 kind: FormalParamKind arity: 0
SymbolTable: non-null
| Body:
| | *OpApplNode: $Case uid: 254 kind: OpApplKind errors: non-null
| | | Operator: $Case 82
| | | Operands: 3
| | | | *OpApplNode: $Pair uid: 246 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | *OpApplNode: < uid: 243 kind: OpApplKind errors: non-null
| | | | | | *OpApplNode: -. uid: 245 kind: OpApplKind errors: non-null
| | | | *OpApplNode: $Pair uid: 251 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | *OpApplNode: = uid: 249 kind: OpApplKind errors: non-null
| | | | | | *NumeralNode: uid: 250 kind: NumeralKind Value: 0; image: 0
| | | | *OpApplNode: $Pair uid: 253 kind: OpApplKind errors: non-null
| | | | | Operator: $Pair 96
| | | | | Operands: 2
| | | | | | null
| | | | | | *NumeralNode: uid: 252 kind: NumeralKind Value: 1; image: 1
Labels: null

Arity: 1
Level: 0
LevelParams: []
LevelConstraints: { }
ArgLevelConstraints: { }
ArgLevelParams: {}
MaxLevel: 2
opLevelCond: [ [ []]]
AllParams: {}
NonLeibnizParams: {}
IsLeibniz: true
isLeibnizArg: true

As can be seen, the null comes from the following construct:
OpApplNode: Operator: $Case - Operands: 3(,,OpApplNode: Operator: $Pair - Operands: 2(null,_))

Unfortunately, the TreeNode representing this semantic node cannot refer to its parents, so there is not obvious way to check the parents of a null operand (to see if it is $Case)> therefore, we have the following ugly fix:
In OpApplNode, we look for the $Case operator and confirm that the third operand is $Pair, then we confirm that the first operands is null. In this case we override the functionality of the xml exporting of these objects. Hopefully, in the future null wont be used as a semantical object

Right now the null node is replaced by:
<StringNode>$Other</StringNode>

libal wrote Jan 1, 2015 at 10:36 AM

After a discussion with Leslie, it occurs to me that one can just export <StringNode>null</StringNode> anytime a node is null and let the reading application (tlapm) figure out what is meant by this null. I have already implemented the above solution but Martin and Leslie should decide together how they want to proceed with regard to both nullpointer errors.