[pivot] Inadequate return type checking

[eclipse-ocl-bot]

| --- | --- | | Bugzilla Link | 582381 | | Status | NEW | | Importance | P3 normal | | Reported | Sep 07, 2023 04:35 EDT | | Modified | Sep 08, 2023 12:09 EDT | | Reporter | Ed Willink |

Description

https://www.eclipse.org/forums/index.php?t=msg&th=1113550&goto=1860766&#msg_1860766 reports that the inadvertent return of self as Boolean in the following is undiagnosed.

def: isTypeOrSpecializationOf(t: ConceptualEntity): Boolean =\ self = t or self?.specializes.isTypeOrSpecializationOf(t)

self is never null so presumably

 self.specializes?.isTypeOrSpecializationOf(t)

was meant. Whatever, a repro can be established by tweaking testValidate_Bug418552_oclinecore to add

operation f() : Boolean[1] { derived }\
{ \
    body: let t : Tester = null in t?.f(); \
} 

There is no validation diagnostic.

[eclipse-ocl-bot]

By Ed Willink on Sep 07, 2023 05:35

For a change the bug is in the auto-generated OCL-defined code. It demonstrates the same bug:

context TypedElement\ def: CompatibleBody(bodySpecification : ValueSpecification[1]) : Boolean[1] =\ bodySpecification.type?.conformsTo(self.type)

The "?." just converts a null-navigation-crash to a null-return-crash.

The [1] target multiplicity requires a stronger test to ensure that a non-null value is returned. Something like

let bodyType = bodySpecification.type\ in (bodyType <> null) and (self.isRequired implies bodyType.isNonNull())

(Once we have built the fix, we should detect that the current Pivot.ocl has this bug too.)

[eclipse-ocl-bot]

By Ed Willink on Sep 07, 2023 11:29

(In reply to Ed Willink from comment #1)

Something like

or rather

def: CompatibleBody(bodySpecification : ExpressionInOCL[1]) : Boolean[1] =\ let bodyType = bodySpecification.type in\ let ownedBody = bodySpecification.ownedBody in\ (bodyType <> null) and (ownedBody <> null) and\ bodyType.conformsTo(self.type) and\ (self.isRequired implies ownedBody.isNonNull())

gives 2 errors and 10 failures for the JUnit tests; some due to test hanrness limitations but e.g for RoyalAndLoyal.ocl we now get 4 warnings. 2 appear reasonable, but 2 indicate indaequate forAll/iterate return types.

Checking RoyalAndLoyal.ecore against 'the book' there are quite a few multiplicity errors. Many underspecified 'attributes' such as 'isMale' are [?] when [1] is obviously intended, and many more such as 'name' are assumed to be [1]. Fixing these seems to make no real difference. The main design error is that Membership.account is explicitly [0..1]. This is reasonable but fails without the safe-navigation on

context TransactionReport::balance : Integer\ derive balance:\ self.card.Membership.account?.points

Now we fail since the 'safe'ly navigated null is not a valid non-null Integer balance. Clarifying balance as Integer[?] would avoid the problem but cannot have been intended. This is clearly a bug in 'the book' that we are chasing around as we improve checking.

How do we fix 'the book'? It seems reasonable that the balance of a TransactionReport with a null account should be zero.

context TransactionReport::balance : Integer\ derive balance:\ let account = self.card.Membership.account in\ if account <> null then account.points else 0 endif

For number, 0 is not so good so use null, rather than -1, as an error

context TransactionReport::number : Integer[?]\ derive number:\ self.card.Membership.account?.number

[eclipse-ocl-bot]

By Ed Willink on Sep 08, 2023 05:32

(In reply to Ed Willink from comment #2)

indicate inadequate forAll/iterate return types.

Simplistically we just implement the missing LibraryIterationOrOperation.resolveReturnNullity overload for each Operation/Iteration for which we can determine a non-null return. However the obvious implementation such as

return PivotUtil.getOwnedBody((IteratorExp)callExp).isNonNull();

doesn't work reliably when invoked in the Left2Right pass since the containment hierarchy is not yet complete and so a non-trivial FlowAnalysis may malfunction.

Ideally we would use the new symbolic evaluation, but that's not yet merged. For now we must persevere with the FlowAnalysis and introduce a further CS2AS pass to touch up the nullity of the complete expression tree.

[eclipse-ocl-bot]

By Ed Willink on Sep 08, 2023 11:24

(In reply to Ed Willink from comment #3)\ ]> return PivotUtil.getOwnedBody((IteratorExp)callExp).isNonNull();\

doesn't work reliably when invoked in the Left2Right pass

Indeed so use .isRequired() which supports usage during the tree climb.

gives 2 errors and 10 failures for the JUnit tests

once we clean up and change referredXXXX to [1] just one fail remains.

In

operation nameLabel(name : String[?]) : String[1]\ {\ body: if name = null then 'null' else name endif;\ }

Better than tree climb isRequired to exploit the guard.

Running comprehensive FloAnalysis just in case would be very expensive. Can we make an oclAsType cast work for analysis inadequacies or do we need an assert?

[eclipse-ocl-bot]

By Ed Willink on Sep 08, 2023 12:09

(In reply to Ed Willink from comment #4)

Can we make an oclAsType cast work for analysis inadequacies or do we need an assert?

oclAsType(String) works fine. So done.

Pushed to ewillink/582381

Hard to merge to master till we can break APIs.