Harden Period creation and use of Run/PhaseId#25484
Harden Period creation and use of Run/PhaseId#25484SolalPirelli wants to merge 7 commits intoscala:mainfrom
Conversation
| if typerPhase.period == Periods.InvalidPeriod then | ||
| getMember(owner, innerName.toTypeName) | ||
| else | ||
| atPhase(typerPhase)(getMember(owner, innerName.toTypeName)) |
There was a problem hiding this comment.
atPhase with an uninitialized phase.
| */ | ||
| def initial: SingleDenotation = | ||
| if (validFor.firstPhaseId <= 1) this | ||
| if (validFor.firstPhaseId == FirstPhaseId) this |
There was a problem hiding this comment.
cannot be == 0 here unless something has gone terribly wrong
| */ | ||
| def skipRemoved(using Context): SingleDenotation = | ||
| if (validFor.code <= 0) nextDefined else this | ||
| if (validFor == Nowhere) nextDefined else this |
There was a problem hiding this comment.
code is nonnegative
| end goBack | ||
|
|
||
| if valid.code <= 0 then | ||
| if valid == Nowhere then |
There was a problem hiding this comment.
code is nonnegative
| * last phase id: 7 bits | ||
| * #phases before last: 7 bits | ||
| * | ||
| * // Dmitry: sign == 0 isn't actually always true, in some cases phaseId == -1 is used for shifts, that easily creates code < 0 |
There was a problem hiding this comment.
no longer true
| case InitialPeriod => "InitialPeriod" | ||
| case InvalidPeriod => "InvalidPeriod" | ||
| case Period(NoRunId, 0, PhaseMask) => s"Period(NoRunId.all)" | ||
| case Period(runId, 0, PhaseMask) => s"Period($runId.all)" |
There was a problem hiding this comment.
this + the next few diffs: no reason to use 0 as the first phase ID to say all when we already have a constant defined to mean that
There was a problem hiding this comment.
also, PhaseMask is logically the wrong thing here, even though it's equivalent to MaxPossiblePhaseId
| } | ||
| } | ||
|
|
||
| inline val NowhereCode = 0 |
There was a problem hiding this comment.
moved down so earlier vals don't depend on later ones
| import scala.collection.mutable.ListBuffer | ||
| import dotty.tools.dotc.transform.MegaPhase.* | ||
| import dotty.tools.dotc.transform.* | ||
| import Periods.* |
There was a problem hiding this comment.
duplicate import with line 5
| && ctx.phaseId <= denot.validFor.lastPhaseId | ||
| && lastDenot != null | ||
| && lastDenot.validFor.lastPhaseId > denot.validFor.firstPhaseId | ||
| && denot.validFor.firstPhaseId < lastDenot.validFor.lastPhaseId |
There was a problem hiding this comment.
| given runContext[Dummy_so_its_a_def]: Context = | ||
| if myCtx eq null then myCtx = rootContext(using ictx) | ||
| assert(myCtx.nn.runId <= Periods.MaxPossibleRunId) | ||
| myCtx.nn |
There was a problem hiding this comment.
reset would leave the run in an invalid state since it sets myCtx to null but there was no code to re-initialize it (in practice we never actually reuse a run that we've reset so this didn't cause problems)
| this.code < that.code | ||
|
|
||
| inline def >(that: Period): Boolean = | ||
| this.code > that.code |
There was a problem hiding this comment.
I didn't dare make these virtual methods in any way because of perf concerns, but I also don't think any code outside of Period should be accessing its .code
96a7fe5 to
e622291
Compare
|
Found even more bugs, will put back in draft until those are fixed + I'm running benchmarks to make sure this doesn't kill perf |
| @@ -0,0 +1,40 @@ | |||
| package dotty.tools.dotc.core | |||
There was a problem hiding this comment.
noticed there was a worksheet testing Period, so I ported it to actual tests
| // lastDiff + d2 <= d1 | ||
| // iff X == 0 && l1 - l2 >= 0 && l1 - l2 + d2 <= d1 | ||
| // iff r1 == r2 & l1 >= l2 && l1 - d1 <= l2 - d2 | ||
| // q.e.d |
There was a problem hiding this comment.
this proof was wrong, counter-example this = (1, 56, 1), that = (1, 51, 32), found by Z3 with:
(declare-fun r1 () (_ BitVec 17))
(declare-fun l1 () (_ BitVec 7))
(declare-fun d1 () (_ BitVec 7))
(declare-fun r2 () (_ BitVec 17))
(declare-fun l2 () (_ BitVec 7))
(declare-fun d2 () (_ BitVec 7))
; d <= l
(assert (bvule d1 l1))
(assert (bvule d2 l2))
; l < 64
(assert (bvult l1 #b1000000))
(assert (bvult l2 #b1000000))
; r > 0
(assert (bvult #b00000000000000000 r1))
(assert (bvult #b00000000000000000 r2))
(declare-fun code1 () (_ BitVec 32))
(assert (= code1 (concat #b0 r1 l1 d1)))
(declare-fun code2 () (_ BitVec 32))
(assert (= code2 (concat #b0 r2 l2 d2)))
(declare-fun phaseWidth () (_ BitVec 32))
(declare-fun phaseMask () (_ BitVec 32))
(assert (= phaseWidth #x00000007))
(assert (= phaseMask #x0000007F))
(declare-fun lastDiff () (_ BitVec 32))
(assert (= lastDiff (bvlshr (bvsub code1 code2) phaseWidth)))
(declare-fun result () Bool)
(assert (= result (bvsle (bvadd lastDiff (bvand code1 phaseMask)) (bvand code2 phaseMask))))
(declare-fun ideal () Bool)
(assert (= ideal (and (= r1 r2) (bvuge l1 l2) (bvule (bvsub l1 d1) (bvsub l2 d2)))))
(assert (not (= result ideal)))
(check-sat)
(get-model)
| def runId: RunId = code >>> (PhaseWidth * 2) | ||
|
|
||
| /** The phase identifier of this single-phase period. */ | ||
| def phaseId: PhaseId = (code >>> PhaseWidth) & PhaseMask |
There was a problem hiding this comment.
this was used on periods with more than one phase... but in practice it seems it's used as a "first phase ID", so I modified callers to just use that
d465112 to
877fc2c
Compare
Found while investigating #24970 but unfortunately does not fix that problem.
How much have your relied on LLM-based tools in this contribution?
not
How was the solution tested?
existing tests