search

UCSD-PL / refscript

Refinement Types for Scripting Languages
BSD 3-Clause "New" or "Revised" License
65 stars 3 forks source link

Fix crash #80

Closed panagosg7 closed 10 years ago

panagosg7 commented 10 years ago

This restores tests: tests/pos/misc/formerly-crashing.ts and tests/neg/misc/formerly-crashing.ts

The problem was with the copying of refinements at UpCasts:

In the following upcast:

p :: Point<int> UP { x: int }

Any refinements associated with the LHS Point would expect the base variable v to be of sort Point. When copied over to the RHS v becomes of sort Object. v could just be part of a substitution, which could cause bogus predicates to appear.

The fix is to substitute the base value v for p when moving refinements from LHS to RHS.

NOTE: This only happens for the top level refinements and only for Upcasts (not downcasts). It addresses the two offending tests cases but might break down the way.

Also fixed an issue on overload resolution based on the number of args of function arguments.

ranjitjhala commented 10 years ago

I think this will cause pain down the line :)

panagosg7 commented 10 years ago

Had you ever dealt with copying refinements of one type over to another with a different sort?