[validation] Deep safe navigation

[eclipse-ocl-bot]

| --- | --- | | Bugzilla Link | 467339 | | Status | RESOLVED FIXED | | Importance | P3 normal | | Reported | May 14, 2015 11:56 EDT | | Modified | Jul 30, 2017 14:30 EDT | | Depends on | 509230 | | Blocks | 507628 | | See also | 509655 | | Reporter | Ed Willink |

Description

Naive vaidation rules for:

if x.oclIsUndefined() then ... else x.something... endif

report an unsafe navigation for x.something.

To avoid trivial irritating warnings, the validation must involve a deep analysis of whether x is non-null.

[eclipse-ocl-bot]

By Ed Willink on Dec 14, 2016 10:23

After adding WFRs for QVTd, the inadequate analysis of implicit in particular is really irritating. There are a significant numbe of warnings of 'unsafe' accesses that are safe.

Is it sufficient to lazily compute at each expression node a

Map from VariableDeclaration to known value, null if known as null, no-entry if not known. An IteratorVariable value is never known; its nullity is declared.

This can be computed by simple bottom up propagation of all values. (Could be finer-grained but then expressions will keep asking for more.)

It can be used by searching up from through container terms to find a known value.

---

Philosophically, if this is to be modelled, we need to add a getKnownValues() operation to each library operation! More generally pre-condition, post-condition, body could all be generalized as named capability definitions.

e.g. in Complete OCL

def: myOp() : T\ cap body: operation=body\ cap precondition: operation pre-condition\ cap staticEvaluation: computation of statically known values.

[eclipse-ocl-bot]

By Ed Willink on Dec 15, 2016 04:49

(In reply to Ed Willink from comment #1)

Is it sufficient to lazily compute at each expression node a

Map from VariableDeclaration to known value, null if known as null, no-entry if not known. An IteratorVariable value is never known; its nullity is declared.

No. That only helps for the degenerate constant-folding problem.

As a consequence of if's and Boolean laws, certain expressions are known to be true at particular places in the control flow. e.g. Consider

if ((x <> null) and (y <> null)) then x.f() else y.f() endif

For x.f() we know that

(x <> null) and (y <> null) = true

which normalizes to

(x <> null) = true\
(y <> null) = true

therefore consideration of the "x is not null" hypothesis finds a confirmation in "(x <> null) = true". "x.f()" is therefore safe.

For y.f() we know that

(x <> null) and (y <> null) = false

which normalizes to

(x = null) or (y = null) = true

and consideration of the "y is not null" hypothesis finds neither confirmation nor contradiction. "y.f()" is therefore unsafe.

In general, safety analysis of var.nav requires a set of Boolean equations to be extracted identifying everything that is known in the context of the var.nav evaluation. The equations can be normalized to "= true" form. "var <> null" can then be substituted and the Boolean consequences followed for each equation to see whether a confirmation or contradiction arises.

?? contradiction wins over confirmation ??

if ((x = null) and (x <> null)) then x.f() else x.g() endif

"everything that is known" may gradually expand as analysis improves. e.g.

some variables are known to be non-null\ some (Integer) iterator variables can be bounded by known iteration domains

"consequences followed" can eventually expand to, substituting the hypotheses, performing constant folding and then merging equations to elaborate partial confirmations/contradictions.

[eclipse-ocl-bot]

By Ed Willink on Dec 22, 2016 18:42

A new FlowAnalysis provides quite strong capabilities for non/non-null propagation. Pushed to master for M5.

Useful *.ocl can b=now be warning free. Raise another bug when stronger anlysis is actually needed.

Bug 509655 identifies an improvement/generalization.

[eclipse-ocl-bot]

By Ed Willink on Jul 30, 2017 14:30

Another couple of keywords to help with Bugzilla searching:

implies, guard