search

SWI-Prolog / packages-pengines

Pengines: Prolog engines
11 stars 13 forks source link

treatment of call/n in static analysis #29

Open Anniepoo opened 7 years ago

Anniepoo commented 7 years ago

In swish

  1. Query ?-call(member, Y, [a,b]). EXPECTED AND OBSERVED: shows a, waits

  2. query ?- X=member,call(X, Y, [a,b]). EXPECTED: same behavior OBSERVED: X=member,call(X, Y, [a,b]). Arguments are not sufficiently instantiated Reachable from: '$swish wrapper'(A,B)

This is apparently a failure of the static analyzer to realize that X must be member by the time the call occurs.

Thanks to our official QA department, Vladislav Zorov, for this.

JanWielemaker commented 7 years ago

If I recall correctly, it used to do this. However, when introducing disjunctions this easily leads to exponential blowup of the analysis. Static analysis can only do so much. If we want full support of (notably) meta-calling we will need runtime sandboxing. I'm not sure whether and how this can be realised without runtime overhead for not sandboxed execution and without complicating the VM too much.

Thinking about a proper explanation why some code cannot be proved safe might be achievable.