import { List , Map , Record , Set } from 'immutable' ; import { getFileInfo } from 'pyright-internal/analyzer/analyzerNodeInfo' ; import { ParseNode , ParseNodeType } from 'pyright-internal/parser/parseNodes' ; import { fetchAddr , genTensor } from './backUtils' ; import { ConstraintSet } from './constraintSet' ; import { Constraint , ConstraintType , CtrAnd , CtrBroad , CtrEq , CtrFail , CtrForall , CtrLt , CtrLte , CtrNeq , CtrNot , CtrOr , ctrToStr , extractSymbols , } from './constraintType' ; import { isStructuallyEq , simplifyExp , simplifyShape } from './expUtils' ; import { NumRange } from './range' ; import { ShEnv , ShHeap } from './sharpEnvironments' ; import { CodeSource , ShContFlag , ShValue , SVAddr , SVBool , SVError , SVErrorLevel , SVFloat , SVFunc , SVInt , SVNone , SVObject , SVSize , SVString , SVType , } from './sharpValues' ; import { ExpBool , ExpNum , ExpNumSymbol , ExpShape , ExpShapeConst , NumBopType , SymBool , SymExp , SymFloat , SymInt , SymShape , SymString , } from './symExpressions' ; import { TorchBackend } from './torchBackend' ; export type CtxExpr = ContextSet < ShValue > ; export type CtxStmt = ContextSet < ShValue | ShContFlag > ; let _failId = 0 ; function getFailedId ( ) { return ++ _failId ; } const LOG_IGNORE = /pylib.*(tensor|functional|builtins|linear|module|loss|math).py$/ ; function checkIgnorePath ( path ) { return LOG_IGNORE . test ( path ) ; } interface ContextProps < T > { failId : number ; env : ShEnv ; heap : ShHeap ; ctrSet : ConstraintSet ; retVal : T ; callStack : List < [ SVFunc | string , CodeSource | undefined ] > ; logs : List < ShValue > ; imported : ShEnv ; relPath : string ; failed ? : SVError ; } interface ContextMethods < T > { toSet ( ) : ContextSet < T > ; toSetWith < A > ( retVal ) : ContextSet < A > ; setEnv ( env ) : Context < T > ; setHeap ( heap ) : Context < T > ; setCtrSet ( ctrSet ) : Context < T > ; setRetVal < A > ( retVal ) : Context < A > ; setRelPath ( relPath ) : Context < T > ; setImported ( imported ) : Context < T > ; getAttrDeep ( value , attr , source ) : ContextSet < ShValue > ; getIndiceDeep ( value , index , source ) : ContextSet < ShValue > ; getKeyValDeep ( value , key , source ) : ContextSet < ShValue > ; addLog ( message , source ) : Context < T > ; addLogValue ( log ) : Context < T > ; pushCallStack ( stack ) : Context < T > ; popCallStack ( ) : Context < T > ; warn ( warning ) : Context < SVError > ; warnWithMsg ( message , source ) : Context < SVError > ; warnSize ( warning ) : Context < SVSize > ; warnSizeWithMsg ( message , source ) : Context < SVSize > ; warnTensor ( warning ) : ContextSet < ShValue > ; warnTensorWithMsg ( message , source ) : ContextSet < ShValue > ; fail ( error ) : Context < SVError > ; failWithMsg ( message , source ) : Context < SVError > ; genList ( values , source ) : [ SVObject , SVAddr , Context < T > ] ; genTuple ( values , source ) : [ SVObject , SVAddr , Context < T > ] ; genSymInt ( name , source ) : SymInt ; genSymFloat ( name , source ) : SymFloat ; genSymBool ( name , source ) : SymBool ; genSymString ( name , source ) : SymString ; genSymShape ( name , rank , source ) : SymShape ; genIntGte ( name , value , source ) : Context < ExpNumSymbol > ; genFloatGte ( name , value , source ) : Context < ExpNumSymbol > ; genConstRankedShape ( rank , source , partialDims ? ) : ContextSet < ExpShapeConst > ; genRankedShape ( rank , source ) : ContextSet < ExpShape > ; genBool ( pred , source ) : Constraint ; genEq ( left , right , source ) : CtrEq ; genNeq ( left , right , source ) : CtrNeq ; genLt ( left , right , source ) : CtrLt ; genLte ( left , right , source ) : CtrLte ; genAnd ( left , right , source ) : CtrAnd ; genOr ( left , right , source ) : CtrOr ; genNot ( constraint , source ) : CtrNot ; genForall ( symbol , range , constraint , source ) : CtrForall ; genBroadcastable ( left , right , source ) : CtrBroad ; genFail ( reason , source ) : CtrFail ; parseSize ( iterable , source ) : ContextSet < ExpShape | string > ; shMatmul ( left , right , source ) : ContextSet < ExpShape > ; shBroadcast ( left , right , source ) : ContextSet < ExpShape > ; shReduce ( shape , axis , source ) : ContextSet < ExpShape > ; shRepeat ( shape , axis , count , source ) : ContextSet < ExpShape > ; require ( ctr , failMsg , source ) : ContextSet < T | SVError > ; guarantee ( ctr ) : Context < T > ; ifThenElse ( ctr , source ) : [ ContextSet < T > , ContextSet < T > ] ; getCachedRange ( num ) : NumRange | undefined ; checkImmediate ( constraint ) : boolean | undefined ; hasPathCtr ( ) : boolean ; isTimedOut ( ) : boolean ; } export interface ContextSet < T > { env : false ; setCtxList < A > ( ctxList ) : ContextSet < A > ; filter ( tester ) : ContextSet < T > ; map < A > ( mapper ) : ContextSet < A > ; flatMap < A > ( mapper ) : ContextSet < A > ; return < A > ( retVal ) : ContextSet < A > ; fail ( errMsg , source ) : ContextSet < SVError > ; join < A > ( ctxSet ) : ContextSet < A | T > ; require ( ctr , failMsg , source ) : ContextSet < T | SVError > ; guarantee ( ctr ) : ContextSet < T > ; ifThenElse ( ctr , source ) : [ ContextSet < T > , ContextSet < T > ] ; getList ( ) : List < Context < T > > ; getFailed ( ) : List < Context < SVError > > ; getStopped ( ) : List < Context < SVError > > ; getRunningCount ( ) : number ; isEmpty ( ) : boolean ; addLog ( message , source ) : ContextSet < T > ; addLogValue ( value ) : ContextSet < T > ; prunePureFunctionCall ( oldCtx , symIdMax ) : ContextSet < T > ; } const contextDefaults = { failId : - 1 , env : new ShEnv ( ) , heap : new ShHeap ( ) , ctrSet : new ConstraintSet ( ) , retVal : undefined , callStack : List ( ) , logs : List ( ) , imported : new ShEnv ( ) , relPath : '.' , failed : undefined , } ; export class Context < T > extends Record ( contextDefaults ) implements ContextProps < T > , ContextMethods < T > { retVal ! : T ; constructor ( values ? ) { values ? super ( values ) : super ( ) ; } setEnv ( env ) { return this . set ( 'env' , env ) ; } setHeap ( heap ) { return this . set ( 'heap' , heap ) ; } setCtrSet ( ctrSet ) { return this . set ( 'ctrSet' , ctrSet ) ; } setRetVal < A > ( retVal ) { return ( ( this as unknown ) as Context < A > ) . set ( 'retVal' , retVal ) ; } setRelPath ( relPath ) { return this . set ( 'relPath' , relPath ) ; } setImported ( imported ) { return this . set ( 'imported' , imported ) ; } getAttrDeep ( value , attr , source ) { return TorchBackend . getAttrDeep ( this , value , attr , source ) ; } getIndiceDeep ( value , index , source ) { return TorchBackend . getIndiceDeep ( this , value , index , source ) ; } getKeyValDeep ( value , key , source ) { return TorchBackend . getKeyValDeep ( this , value , key , source ) ; } warn ( warning ) { return this . setRetVal ( warning ) . addLogValue ( warning ) ; } warnWithMsg ( message , source ) { source = this . _replaceBuiltinSource ( source ) ; const warning = SVError . create ( message , SVErrorLevel . Warning , source ) ; return this . setRetVal ( warning ) . addLogValue ( warning ) ; } warnTensor ( warning ) { const ctx = this . addLogValue ( warning ) ; const source = warning . source ; const rank = ctx . genSymInt ( 'WarnTempRank' , source ) ; const shape = ctx . genSymShape ( 'WarnTempShape' , ExpNum . fromSymbol ( rank ) , source ) ; return genTensor ( ctx , ExpShape . fromSymbol ( shape ) , source ) ; } warnTensorWithMsg ( message , source ) { const warning = SVError . create ( message , SVErrorLevel . Warning , source ) ; return this . warnTensor ( warning ) ; } warnSize ( warning ) { const ctx = this . addLogValue ( warning ) ; const source = warning . source ; const rank = ctx . genSymInt ( 'WarnTempRank' , source ) ; const shape = ctx . genSymShape ( 'WarnTempShape' , ExpNum . fromSymbol ( rank ) , source ) ; return SVSize . createSize ( ctx , ExpShape . fromSymbol ( shape ) , source ) ; } warnSizeWithMsg ( message , source ) { const warning = SVError . create ( message , SVErrorLevel . Warning , source ) ; return this . warnSize ( warning ) ; } fail ( error ) { return this . set ( 'failed' , error ) . set ( 'failId' , getFailedId ( ) ) . addLogValue ( error ) . setRetVal ( error ) ; } failWithMsg ( message , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . fail ( SVError . create ( message , SVErrorLevel . Error , source ) ) ; } addLog ( message , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . set ( 'logs' , this . logs . push ( SVError . create ( message , SVErrorLevel . Log , source ) ) ) ; } addLogValue ( log ) { return this . set ( 'logs' , this . logs . push ( log ) ) ; } pushCallStack ( stack ) { return this . set ( 'callStack' , this . callStack . push ( stack ) ) ; } popCallStack ( ) { return this . set ( 'callStack' , this . callStack . pop ( ) ) ; } toSet ( ) { return ContextSetImpl . fromCtx ( this ) ; } toSetWith < A > ( retVal ) { return ContextSetImpl . fromCtx ( this . setRetVal ( retVal ) ) ; } static getEmptySet ( ) { return new ContextSetImpl ( List ( ) ) ; } asDefault ( ) { const offset = - this . heap . addrMax - 1 ; return this . setEnv ( this . env . addOffset ( offset ) ) . setHeap ( this . heap . addOffset ( offset ) ) ; } genList ( values , source ) { const { heap , env } = this ; const [ list , listAddr , heap2 ] = SVObject . create ( heap , source ) ; const listMro = ( fetchAddr ( heap . getVal ( env . getId ( 'list' ) ! ) ! , heap ) as SVObject ) . getAttr ( '__mro__' ) ! ; let listVal = list ; values . forEach ( ( v , i ) => { listVal = listVal . setIndice ( i , v ) ; } ) ; listVal = listVal . setAttr ( '$length' , SVInt . create ( values . length , source ) ) . setAttr ( '__mro__' , listMro ) ; return [ list , listAddr , this . setHeap ( heap2 . setVal ( listAddr , listVal ) ) ] ; } genTuple ( values , source ) { const { heap , env } = this ; const [ tuple , tupleAddr , heap2 ] = SVObject . create ( heap , source ) ; const tupleMro = ( fetchAddr ( heap . getVal ( env . getId ( 'tuple' ) ! ) ! , heap ) as SVObject ) . getAttr ( '__mro__' ) ! ; let listVal = tuple ; values . forEach ( ( v , i ) => { listVal = listVal . setIndice ( i , v ) ; } ) ; listVal = listVal . setAttr ( '$length' , SVInt . create ( values . length , source ) ) . setAttr ( '__mro__' , tupleMro ) ; return [ tuple , tupleAddr , this . setHeap ( heap2 . setVal ( tupleAddr , listVal ) ) ] ; } genSymInt ( name , source ) { return this . ctrSet . genSymInt ( name , source ) ; } genSymFloat ( name , source ) { return this . ctrSet . genSymFloat ( name , source ) ; } genSymBool ( name , source ) { return this . ctrSet . genSymBool ( name , source ) ; } genSymString ( name , source ) { return this . ctrSet . genSymString ( name , source ) ; } genSymShape ( name , rank , source ) { return this . ctrSet . genSymShape ( name , rank , source ) ; } genIntEq ( name , value , source ) { source = this . _replaceBuiltinSource ( source ) ; const [ num , ctrSet ] = this . ctrSet . genSymIntEq ( name , value , source ) ; const exp = ExpNum . fromSymbol ( num ) ; return this . setCtrSet ( ctrSet ) . setRetVal ( exp ) ; } genIntGte ( name , value , source ) { const num = this . genSymInt ( name , source ) ; const exp = ExpNum . fromSymbol ( num ) ; const pos = this . genLte ( value , exp , source ) ; return this . guarantee ( pos ) . setRetVal ( exp ) ; } genFloatGte ( name , value , source ) { const num = this . genSymFloat ( name , source ) ; const exp = ExpNum . fromSymbol ( num ) ; const pos = this . genLte ( value , exp , source ) ; return this . guarantee ( pos ) . setRetVal ( exp ) ; } genConstRankedShape ( rank , source , partialDims ? ) { source = this . _replaceBuiltinSource ( source ) ; if ( rank < 0 ) return ( this . failWithMsg ( `from 'genRankedShape': got negative rank ${ rank }` , source ) . toSet ( ) as ContextSet < unknown > ) as ContextSet < ExpShapeConst > ; const dims = [ ] ; let ctx = this ; for ( let i = 0 ; i < rank ; i ++ ) { const dimPart = partialDims ?. get ( i ) ; if ( dimPart ) { dims . push ( dimPart ) ; continue ; } const minDimPart = partialDims ?. get ( - rank + i ) ; if ( minDimPart ) { dims . push ( minDimPart ) ; continue ; } const temp = ctx . genIntGte ( `tempDim${ i }` , 0 , source ) ; const dim = temp . retVal ; dims . push ( dim ) ; ctx = temp ; } const parts = partialDims ? [ ... partialDims . values ( ) ] : [ ] ; if ( parts . length > 0 ) { return ctx . require ( parts . map ( ( num ) => ctx . genLte ( 0 , num , source ) ) , `from 'genRankedShape': got negative partialDims` , source ) . return ( ExpShape . fromConst ( rank , dims , source ) ) ; } return ctx . setRetVal ( ExpShape . fromConst ( rank , dims , source ) ) . toSet ( ) ; } genRankedShape ( rank , source , partialDims ? ) { source = this . _replaceBuiltinSource ( source ) ; if ( typeof rank === 'number' ) { return this . genConstRankedShape ( rank , source , partialDims ) ; } const rankRng = this . getCachedRange ( rank ) ; if ( ! rankRng || rankRng . lt ( 0 ) ) { return ( this . failWithMsg ( `from 'genRankedShape': invalid rank ${ ExpNum . toString ( rank ) }` , source ) . toSet ( ) as ContextSet < unknown > ) as ContextSet < ExpShape > ; } if ( rankRng . isConst ( ) ) { return this . genConstRankedShape ( rankRng . end , source , partialDims ) ; } const dimValues = partialDims ? [ ... partialDims . values ( ) ] : [ ] ; const ctxSet = dimValues . length > 0 ? this . require ( dimValues . map ( ( num ) => this . genLte ( 0 , num , source ) ) , `from 'genRankedShape': got negative partialDims` , source ) : this . toSet ( ) ; return ctxSet . require ( this . genLte ( 0 , rank , source ) , `genRankedShape got negative rank ${ rank }` , source ) . flatMap ( ( ctx ) => { if ( rankRng . end !== Infinity && rankRng . end <= 20 ) { const rankMax = rankRng . end ; return ctx . genConstRankedShape ( rankMax , source , partialDims ) . map ( ( ctx ) => { const shape = ctx . retVal ; return ctx . setRetVal ( ExpShape . slice ( shape , 0 , rank , source ) ) as Context < ExpShape > ; } ) ; } else { const symShape = ctx . genSymShape ( 'temp' , rank , source ) ; const expShape = ExpShape . fromSymbol ( symShape ) ; let ctxSet = ctx . toSet ( ) ; let retShape = ExpShape . fromSymbol ( symShape ) ; partialDims ?. forEach ( ( dim , idx ) => { const idxExp = idx >= 0 ? ExpNum . fromConst ( idx , source ) : ExpNum . bop ( NumBopType . Sub , rank , idx , source ) ; retShape = ExpShape . setDim ( retShape , idxExp , dim , source ) ; ctxSet = ctxSet . guarantee ( ctx . genEq ( ExpNum . index ( expShape , idxExp , source ) , dim , source ) ) ; } ) ; return ctxSet . return ( ExpShape . fromSymbol ( symShape ) ) ; } } ) ; } genBool ( pred , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genEquality ( ConstraintType . Equal , SymExp . fromConst ( pred ) , SymExp . fromConst ( true ) , source ) as CtrEq ; } genEq ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genEquality ( ConstraintType . Equal , SymExp . fromConst ( left ) , SymExp . fromConst ( right ) , source ) as CtrEq ; } genNeq ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genEquality ( ConstraintType . NotEqual , SymExp . fromConst ( left ) , SymExp . fromConst ( right ) , source ) as CtrNeq ; } genLt ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genNumCompare ( ConstraintType . LessThan , SymExp . fromConst ( left ) as ExpNum , SymExp . fromConst ( right ) as ExpNum , source ) as CtrLt ; } genLte ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genNumCompare ( ConstraintType . LessThanOrEqual , SymExp . fromConst ( left ) as ExpNum , SymExp . fromConst ( right ) as ExpNum , source ) as CtrLte ; } genAnd ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genAnd ( left , right , source ) ; } genOr ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genOr ( left , right , source ) ; } genNot ( constraint , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genNot ( constraint , source ) ; } genBroadcastable ( left , right , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genBroad ( left , right , source ) ; } genForall ( symbol , range , constraint , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genForall ( symbol , range , constraint , source ) ; } genFail ( reason , source ) { source = this . _replaceBuiltinSource ( source ) ; return this . ctrSet . genFail ( reason , source ) ; } parseSize ( iterable , source ) { const sizeObj = fetchAddr ( iterable , this . heap ) ; if ( sizeObj ?. type !== SVType . Object ) { return this . toSetWith ( 'value is not iterable; cannot parse to size.' ) ; } if ( sizeObj instanceof SVSize ) { return this . toSetWith ( sizeObj . shape ) ; } const rankValue = fetchAddr ( sizeObj . getAttr ( '$length' ) , this . heap ) ; if ( rankValue ?. type !== SVType . Int ) { return this . toSetWith ( 'value is not iterable; cannot parse to size.' ) ; } return this . genRankedShape ( rankValue . value , source , sizeObj . extractIndexedNumber ( this . heap ) ) ; } shBroadcast ( left , right , source ) { return this . require ( [ this . genBroadcastable ( left , right , source ) ] , 'shape is not broadcastable' , source ) . return ( simplifyShape ( this . ctrSet , ExpShape . broadcast ( left , right , source ) ) ) ; } shReduce ( shape , axis , source ) { const left = ExpShape . slice ( shape , undefined , axis , source ) ; const right = ExpShape . slice ( shape , ExpNum . bop ( NumBopType . Add , axis , 1 , source ) , undefined , source ) ; let newShape = ExpShape . concat ( left , right , source ) ; newShape = simplifyShape ( this . ctrSet , newShape ) ; return this . setRetVal ( newShape ) . toSet ( ) ; } shMatmul ( left , right , source ) { const ctx = this ; const leftRank = ExpShape . getRank ( left ) ; const rightRank = ExpShape . getRank ( right ) ; const leftMDim = ExpNum . index ( left , ExpNum . bop ( NumBopType . Sub , leftRank , 1 , source ) , source ) ; const rightMDim = ExpNum . index ( right , ExpNum . bop ( NumBopType . Sub , rightRank , 2 , source ) , source ) ; return ctx . require ( [ ctx . genLte ( 2 , leftRank , source ) , ctx . genLte ( 2 , rightRank , source ) ] , `from 'matmul': rank should be greater than 1` , source ) . flatMap ( ( ctx ) => ctx . require ( [ ctx . genEq ( leftMDim , rightMDim , source ) ] , `from 'matmul': dimension mismatch` , source ) ) . flatMap ( ( ctx ) => ctx . shBroadcast ( ExpShape . slice ( left , 0 , ExpNum . bop ( NumBopType . Sub , leftRank , 2 , source ) , source ) , ExpShape . slice ( right , 0 , ExpNum . bop ( NumBopType . Sub , rightRank , 2 , source ) , source ) , source ) ) . map ( ( ctx ) => { const broadShape = ctx . retVal ; const leftLDim = ExpNum . index ( left , ExpNum . bop ( NumBopType . Sub , leftRank , 2 , source ) , source ) ; const rightRDim = ExpNum . index ( right , ExpNum . bop ( NumBopType . Sub , rightRank , 1 , source ) , source ) ; const matmulShape = ExpShape . fromConst ( 2 , [ leftLDim , rightRDim ] , source ) ; return ctx . setRetVal ( simplifyShape ( this . ctrSet , ExpShape . concat ( broadShape , matmulShape , source ) ) ) ; } ) ; } shRepeat ( shape , axis , count , source ) { const rank = ExpShape . getRank ( shape ) ; const axisCtr = this . genAnd ( this . genLte ( 0 , axis , source ) , this . genLte ( axis , rank , source ) , source ) ; const countCtr = this . genLte ( 0 , count , source ) ; return this . require ( [ axisCtr , countCtr ] , 'shRepeat constraint failed' , source ) . map ( ( ctx ) => { const leftShape = ExpShape . slice ( shape , undefined , axis , source ) ; const rightShape = ExpShape . slice ( shape , axis , undefined , source ) ; const repeated = ExpShape . concat ( ExpShape . concat ( leftShape , ExpShape . fromConst ( 1 , [ count ] , source ) , source ) , rightShape , source ) ; return ctx . setRetVal ( simplifyShape ( this . ctrSet , repeated ) ) ; } ) ; } require ( ctr , failMsg , source ) { source = this . _replaceBuiltinSource ( source ) ; if ( Array . isArray ( ctr ) ) { return this . toSet ( ) . require ( ctr , failMsg , source ) ; } else { return this . toSet ( ) . require ( ctr , failMsg , source ) ; } } guarantee ( ctr ) { if ( Array . isArray ( ctr ) ) { return this . setCtrSet ( this . ctrSet . guaranteeAll ( ctr ) ) ; } else { return this . setCtrSet ( this . ctrSet . guarantee ( ctr ) ) ; } } ifThenElse ( ctr , source ) { return this . toSet ( ) . ifThenElse ( ctr , source ) ; } getCachedRange ( num ) { return this . ctrSet . getCachedRange ( num ) ; } checkImmediate ( constraint ) { return this . ctrSet . checkImmediate ( constraint ) ; } hasPathCtr ( ) { return ! this . ctrSet . pathCtr . isEmpty ( ) ; } isTimedOut ( ) { const reason = this . failed ; if ( reason && reason . reason . startsWith ( 'timeout expired' ) ) { return true ; } return false ; } private _replaceBuiltinSource ( source ) { if ( source && ! ( 'fileId' in source ) ) { let moduleNode = source ; while ( moduleNode . nodeType !== ParseNodeType . Module ) { moduleNode = moduleNode . parent ! ; } const fileInfo = getFileInfo ( moduleNode ) ! ; if ( checkIgnorePath ( fileInfo . filePath ) ) { for ( let i = this . callStack . count ( ) - 1 ; i >= 0 ; i -- ) { const node = this . callStack . get ( i ) ! [ 1 ] ; if ( node && ! ( 'fileId' in node ) ) { moduleNode = node ; while ( moduleNode . nodeType !== ParseNodeType . Module ) { moduleNode = moduleNode . parent ! ; } const fileInfo = getFileInfo ( moduleNode ) ! ; if ( ! checkIgnorePath ( fileInfo . filePath ) ) { return node ; } } } } } return source ; } } export namespace ContextSet { export type CtxConstructorCallback = ( ctxSet : ContextSetImpl < unknown > ) => void ; let _callbacks = [ ] ; let _maxPaths = 0 ; export function clearCallbacks ( ) { _callbacks = [ ] ; } export function setCallback ( callback ) { _callbacks . push ( callback ) ; } export function checkCallbacks ( ctxSet ) { for ( const callback of _callbacks ) { callback ( ctxSet ) ; } } export function getMaxPaths ( ) { return _maxPaths ; } export function setMaxPaths ( count ) { _maxPaths = count ; } } export class ContextSetImpl < T > implements ContextSet < T > { env : false ; ctxList : List < Context < T > > ; failed : List < Context < SVError > > ; stopped : List < Context < SVError > > ; constructor ( ctxList , failed ? , stopped ? ) { this . env = false ; this . ctxList = ctxList ; this . failed = failed ? failed : List ( ) ; this . stopped = stopped ? stopped : List ( ) ; ContextSet . checkCallbacks ( this ) ; } static fromCtx < A > ( ctx ) { if ( ctx . failed ) { let failedCtx = ctx . setRetVal ( ctx . failed ) ; if ( failedCtx . failId === - 1 ) { failedCtx = failedCtx . set ( 'failId' , getFailedId ( ) ) ; } if ( failedCtx . hasPathCtr ( ) ) { return new ContextSetImpl ( List ( ) , List ( ) , List ( [ failedCtx ] ) ) ; } else { return new ContextSetImpl ( List ( ) , List ( [ failedCtx ] ) , List ( ) ) ; } } else { return new ContextSetImpl ( List ( [ ctx ] ) , List ( ) , List ( ) ) ; } } getList ( ) { return this . ctxList ; } getFailed ( ) { return this . failed ; } getStopped ( ) { return this . stopped ; } getRunningCount ( ) { return this . ctxList . count ( ) ; } filter ( tester ) { return new ContextSetImpl ( this . ctxList . filter ( tester ) , this . failed , this . stopped ) ; } setCtxList < A > ( ctxList ) { const succeed = ctxList . filter ( ( ctx ) => ctx . failed === undefined ) ; const failed = ctxList . filter ( ( ctx ) => ctx . failed !== undefined ) . filter ( ( ctx ) => ! ctx . hasPathCtr ( ) ) . map ( ( ctx ) => { let failed = ctx . setRetVal ( ctx . failed ! ) ; if ( ctx . failId === - 1 ) failed = failed . set ( 'failId' , getFailedId ( ) ) ; return failed ; } ) ; const stopped = ctxList . filter ( ( ctx ) => ctx . failed !== undefined ) . filter ( ( ctx ) => ctx . hasPathCtr ( ) ) . map ( ( ctx ) => { let stopped = ctx . setRetVal ( ctx . failed ! ) ; if ( ctx . failId === - 1 ) stopped = stopped . set ( 'failId' , getFailedId ( ) ) ; return stopped ; } ) ; return new ContextSetImpl ( succeed , this . failed . concat ( failed ) , this . stopped . concat ( stopped ) ) ; } map < A > ( mapper ) { return this . setCtxList ( this . ctxList . map ( mapper ) ) ; } flatMap < A > ( mapper ) { const mapped = this . ctxList . map ( mapper ) ; const succeed = mapped . toArray ( ) . flatMap ( ( cs ) => cs . getList ( ) . toArray ( ) ) ; const failed = mapped . toArray ( ) . flatMap ( ( cs ) => cs . getFailed ( ) . toArray ( ) ) ; const stopped = mapped . toArray ( ) . flatMap ( ( cs ) => cs . getStopped ( ) . toArray ( ) ) ; return new ContextSetImpl ( List ( succeed ) , List ( failed ) . concat ( this . failed ) , List ( stopped ) . concat ( this . stopped ) ) ; } return < A > ( retVal ) { return new ContextSetImpl ( this . ctxList . map ( ( ctx ) => ctx . setRetVal ( retVal ) ) , this . failed , this . stopped ) ; } fail ( errMsg , source ) { return new ContextSetImpl ( List ( ) , this . ctxList . filter ( ( ctx ) => { ! ctx . hasPathCtr ( ) ; } ) . map ( ( ctx ) => { return ctx . failWithMsg ( errMsg , source ) ; } ) . concat ( this . failed ) , this . ctxList . filter ( ( ctx ) => { ctx . hasPathCtr ( ) ; } ) . map ( ( ctx ) => { return ctx . failWithMsg ( errMsg , source ) ; } ) . concat ( this . stopped ) ) ; } join < A > ( ctxSet ) { const thisList = this . ctxList ; const thatList = ctxSet . getList ( ) ; const failedSet = { } ; const thatFailed = ctxSet . getFailed ( ) ; this . failed . forEach ( ( ctx ) => ( failedSet [ ctx . failId ] = ctx ) ) ; thatFailed . forEach ( ( ctx ) => ( failedSet [ ctx . failId ] = ctx ) ) ; const stoppedSet = { } ; const thatStopped = ctxSet . getStopped ( ) ; this . stopped . forEach ( ( ctx ) => ( stoppedSet [ ctx . failId ] = ctx ) ) ; thatStopped . forEach ( ( ctx ) => ( stoppedSet [ ctx . failId ] = ctx ) ) ; return new ContextSetImpl ( thisList . concat ( thatList ) , List ( Object . values ( failedSet ) ) , List ( Object . values ( stoppedSet ) ) ) ; } require ( ctr , failMsg , source ) { const ctrList = Array . isArray ( ctr ) ? ctr . map ( ( c ) => ( { ... c , message : failMsg } ) ) : [ { ... ctr , message : failMsg } ] ; return this . map ( ( ctx ) => { const ctrSet = ctx . ctrSet . requireAll ( ctrList ) ; if ( ctrSet . valid === false ) { const ctrMsg = ctrList . map ( ( ctr ) => `${ ctrToStr ( ctr ) }` ) . join ( ' /\\ \n' ) ; const errMsg = `${ failMsg ? failMsg : 'runtime constraint mismatch' }\n  CONSTRAINTS:\n${ ctrMsg }\n` ; return ctx . setCtrSet ( ctrSet ) . failWithMsg ( errMsg , source ) as Context < T | SVError > ; } else { return ctx . setCtrSet ( ctrSet ) ; } } ) ; } guarantee ( ctr ) { return this . map ( ( ctx ) => { if ( Array . isArray ( ctr ) ) { return ctx . setCtrSet ( ctx . ctrSet . guaranteeAll ( ctr ) ) ; } else { return ctx . setCtrSet ( ctx . ctrSet . guarantee ( ctr ) ) ; } } ) ; } ifThenElse ( ctr , source ) { const ifPath = [ ] ; const elsePath = [ ] ; this . ctxList . forEach ( ( ctx ) => { const ctrSet = ctx . ctrSet . addIf ( { ... ctr , message : 'true path' } ) ; if ( ctrSet . valid !== false ) { ifPath . push ( ctx . setCtrSet ( ctrSet ) ) ; } const elseSet = ctx . ctrSet . addIf ( { ... ctx . ctrSet . genNot ( ctr , source ) , message : 'false path' } ) ; if ( elseSet . valid !== false ) { elsePath . push ( ctx . setCtrSet ( elseSet ) ) ; } } ) ; return [ new ContextSetImpl ( List ( ifPath ) , this . failed , this . stopped ) , new ContextSetImpl ( List ( elsePath ) , this . failed , this . stopped ) , ] ; } isEmpty ( ) { return this . ctxList . isEmpty ( ) ; } addLog ( message , source ) { return this . map ( ( ctx ) => ctx . addLog ( message , source ) ) ; } addLogValue ( value ) { return this . map ( ( ctx ) => ctx . addLogValue ( value ) ) ; } prunePureFunctionCall ( oldCtx , symIdMax ) { if ( this . ctxList . count ( ) !== 2 ) return this ; const oldHeap = oldCtx . heap ; const heapLimit = oldHeap . addrMax ; const left = this . ctxList . get ( 0 ) ! ; const right = this . ctxList . get ( 1 ) ! ; const leftSet = left . ctrSet ; const rightSet = right . ctrSet ; const leftLen = leftSet . ctrPool . count ( ) ; const rightLen = rightSet . ctrPool . count ( ) ; const oldSoftLen = oldCtx . ctrSet . softCtr . count ( ) ; if ( leftSet . softCtr . count ( ) !== oldSoftLen || rightSet . softCtr . count ( ) !== oldSoftLen ) { return this ; } if ( leftSet . notPrunedCtrMax >= leftLen ) { const newList = this . ctxList . set ( 1 , right . setCtrSet ( rightSet . set ( 'notPrunedCtrMax' , rightLen ) ) ) ; return new ContextSetImpl ( newList , this . getFailed ( ) , this . getStopped ( ) ) ; } else if ( rightSet . notPrunedCtrMax >= rightLen ) { const newList = this . ctxList . set ( 0 , left . setCtrSet ( leftSet . set ( 'notPrunedCtrMax' , leftLen ) ) ) ; return new ContextSetImpl ( newList , this . getFailed ( ) , this . getStopped ( ) ) ; } const newThis = new ContextSetImpl ( this . ctxList . set ( 0 , left . setCtrSet ( leftSet . set ( 'notPrunedCtrMax' , leftLen ) ) ) . set ( 1 , right . setCtrSet ( rightSet . set ( 'notPrunedCtrMax' , rightLen ) ) ) , this . failed , this . stopped ) ; const oldLen = oldCtx . ctrSet . ctrPool . count ( ) ; for ( let i = oldLen ; i < leftLen ; i ++ ) { const leftSymbols = Set ( extractSymbols ( leftSet . ctrPool . get ( i ) ! ) ) ; if ( leftSymbols . find ( ( v ) => v <= symIdMax ) ?? - 1 >= 0 ) return newThis ; } for ( let i = oldLen ; i < rightLen ; i ++ ) { const rightSymbols = Set ( extractSymbols ( rightSet . ctrPool . get ( i ) ! ) ) ; if ( rightSymbols . find ( ( v ) => v <= symIdMax ) ?? - 1 >= 0 ) return newThis ; } let leftRet = ( left . retVal as any ) as ShValue | ShContFlag ; let rightRet = ( right . retVal as any ) as ShValue | ShContFlag ; const leftHeap = left . heap ; const rightHeap = right . heap ; let eqMap = Map < number , number > ( ) ; if ( typeof leftRet !== 'object' ) leftRet = SVNone . create ( undefined ) ; if ( typeof rightRet !== 'object' ) rightRet = SVNone . create ( undefined ) ; function eqCheck ( lv ? , rv ? ) { if ( lv ?. type === SVType . Addr ) { lv = fetchAddr ( lv , leftHeap ) ; } if ( rv ?. type === SVType . Addr ) { rv = fetchAddr ( rv , rightHeap ) ; } if ( ! lv && ! rv ) return true ; if ( ! ( lv && rv ) ) return false ; if ( lv . type !== rv . type ) return false ; switch ( lv . type ) { case SVType . Int : case SVType . Float : { const lval = lv . value ; const rval = ( rv as SVInt | SVFloat ) . value ; if ( typeof lval === 'number' ) { if ( typeof rval === 'number' ) { return lval === rval ; } return false ; } if ( typeof rval === 'number' ) { return false ; } const lsval = simplifyExp ( leftSet , lval ) ; const rsval = simplifyExp ( rightSet , rval ) ; if ( SymExp . extractSymbols ( lsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; if ( SymExp . extractSymbols ( rsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; return isStructuallyEq ( lsval , rsval ) ; } case SVType . String : { const lval = lv . value ; const rval = ( rv as SVString ) . value ; if ( typeof lval === 'string' ) { if ( typeof rval === 'string' ) { return lval === rval ; } return false ; } if ( typeof rval === 'string' ) { return false ; } const lsval = simplifyExp ( leftSet , lval ) ; const rsval = simplifyExp ( rightSet , rval ) ; if ( SymExp . extractSymbols ( lsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; if ( SymExp . extractSymbols ( rsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; return isStructuallyEq ( lsval , rsval ) ; } case SVType . Bool : { const lval = lv . value ; const rval = ( rv as SVBool ) . value ; if ( typeof lval === 'boolean' ) { if ( typeof rval === 'boolean' ) { return lval === rval ; } return false ; } if ( typeof rval === 'boolean' ) { return false ; } const lsval = simplifyExp ( leftSet , lval ) ; const rsval = simplifyExp ( rightSet , rval ) ; if ( SymExp . extractSymbols ( lsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; if ( SymExp . extractSymbols ( rsval ) . findIndex ( ( v ) => v > symIdMax ) >= 0 ) return false ; return isStructuallyEq ( lsval , rsval ) ; } case SVType . Object : { const rval = rv as SVObject ; const laddr = lv . addr . addr ; const raddr = rval . addr . addr ; if ( laddr <= heapLimit ) { if ( raddr <= heapLimit ) { return laddr === raddr ; } return false ; } else if ( raddr <= heapLimit ) { return false ; } if ( eqMap . has ( laddr ) ) { if ( eqMap . get ( laddr ) !== raddr ) return false ; return true ; } eqMap = eqMap . set ( laddr , raddr ) ; if ( lv . shape ) { if ( ! rval . shape ) return false ; if ( ! isStructuallyEq ( simplifyExp ( leftSet , lv . shape ) , simplifyExp ( rightSet , rval . shape ) ) ) return false ; } if ( lv . keyValues . count ( ) !== rval . keyValues . count ( ) ) return false ; if ( lv . indices . count ( ) !== rval . indices . count ( ) ) return false ; if ( lv . attrs . count ( ) !== rval . attrs . count ( ) ) return false ; if ( ! lv . keyValues . every ( ( lvv , lvk ) => eqCheck ( lvv , rval . keyValues . get ( lvk ) ) ) ) return false ; if ( ! lv . indices . every ( ( lvv , lvk ) => eqCheck ( lvv , rval . indices . get ( lvk ) ) ) ) return false ; if ( ! lv . attrs . every ( ( lvv , lvk ) => eqCheck ( lvv , rval . attrs . get ( lvk ) ) ) ) return false ; return true ; } case SVType . Func : return lv === rv ; case SVType . None : case SVType . NotImpl : case SVType . Undef : return true ; case SVType . Error : return lv === rv ; default : return false ; } } if ( ! eqCheck ( leftRet , rightRet ) ) return newThis ; const pureLeftMap = leftHeap . valMap . filter ( ( _ , addr ) => addr <= heapLimit ) ; const pureRightMap = rightHeap . valMap . filter ( ( _ , addr ) => addr <= heapLimit ) ; const pureMap = oldHeap . valMap . filter ( ( _ , addr ) => addr <= heapLimit ) ; if ( ! ( pureLeftMap . equals ( pureMap ) && pureRightMap . equals ( pureMap ) ) ) { return newThis ; } return left . setCtrSet ( oldCtx . ctrSet ) . toSet ( ) ; } }