package Ġorg . jetbrains . research . k ex . smt . b oo lect or Ċ Ċ import Ġorg . jetbrains . research . b oo lect or . B tor Ċ import Ġorg . jetbrains . research . k ex . config . k ex Config Ċ import Ġorg . jetbrains . research . k ex . k type .* Ċ import Ġorg . jetbrains . research . k ex . smt .* Ċ import Ġorg . jetbrains . research . k ex . state . Predicate State Ċ import Ġorg . jetbrains . research . k ex . state . term .* Ċ import Ġorg . jetbrains . research . k ex . state . transformer . collect Pointers Ċ import Ġorg . jetbrains . research . k ex . state . transformer . collect Types Ċ import Ġorg . jetbrains . research . k ex . state . transformer . collect Variables Ċ import Ġorg . jetbrains . research . k ex . state . transformer . mem space Ċ import Ġorg . jetbrains . research . k fg . type . Type Factory Ċ import Ġorg . jetbrains . research . k the l per . assert . kt assert Ċ import Ġorg . jetbrains . research . k the l per . assert . unreachable Ċ import Ġorg . jetbrains . research . k the l per . logging . log Ċ Ċ private Ġval Ġlog Query Ġ= Ġk ex Config . getBoolean Value (" smt ", Ġ" log Query ", Ġfalse ) Ċ private Ġval Ġlog Form ul ae Ġ= Ġk ex Config . getBoolean Value (" smt ", Ġ" log Form ul ae ", Ġfalse ) Ċ Ċ private Ġtype alias ĠMemory State Ġ= ĠMutable Map < Term , ĠTerm > Ċ private Ġtype alias ĠMemory Pair Ġ= ĠPair < Memory State , ĠMemory State > Ċ Ċ @ Solver (" b oo lect or ") Ċ class ĠB oo lect or Solver ( val Ġtf : ĠType Factory ) Ġ: ĠAbstract S MT Solver Ġ{ ĊĠĠĠ Ġval Ġef Ġ= ĠB oo lect or Expr Factory () ĊĊĠĠĠ Ġoverride Ġfun Ġis Reach able ( state : ĠPredicate State ) Ġ= ĊĠĠĠĠĠĠĠ Ġis Path Possible ( state , Ġstate . path ) ĊĊĠĠĠ Ġoverride Ġfun Ġis Path Possible ( state : ĠPredicate State , Ġpath : ĠPredicate State ) Ġ= Ġis Vi olated ( state , Ġpath ) ĊĊĠĠĠ Ġoverride Ġfun Ġis Vi olated ( state : ĠPredicate State , Ġquery : ĠPredicate State ): ĠResult Ġ{ ĊĠĠĠĠĠĠĠ Ġif Ġ( log Query ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlog . run Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġdebug (" B oo lect or Ġsolver Ġcheck ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġdebug (" State : Ġ$ state ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġdebug (" Query : Ġ$ query ") ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġctx Ġ= ĠB oo lect or Context ( ef , Ġ( 1 Ġshl Ġ 8 ) Ġ+ Ġ 1 , Ġ( 1 Ġshl Ġ 2 4 ) Ġ+ Ġ 1 ) ĊĊĠĠĠĠĠĠĠ Ġval Ġconverter Ġ= ĠB oo lect or Converter ( tf ) ĊĠĠĠĠĠĠĠ Ġconverter . init ( collect Types ( state )) ĊĠĠĠĠĠĠĠ Ġval Ġb oo lect or State Ġ= Ġconverter . convert ( state , Ġef , Ġctx ) ĊĠĠĠĠĠĠĠ Ġval Ġb oo lect or Query Ġ= Ġconverter . convert ( query , Ġef , Ġctx ) ĊĊĠĠĠĠĠĠĠ Ġlog . debug (" Check Ġstarted ") ĊĠĠĠĠĠĠĠ Ġval Ġresult Ġ= Ġcheck ( b oo lect or State , Ġb oo lect or Query ) ĊĠĠĠĠĠĠĠ Ġlog . debug (" Check Ġfinished ") ĊĠĠĠĠĠĠĠ Ġreturn Ġwhen Ġ( result ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ ĠB tor . Status . UN SAT Ġ-> ĠResult . Un sat Result ĊĠĠĠĠĠĠĠĠĠĠĠ ĠB tor . Status . UNKNOWN Ġ-> ĠResult . Unknown Result (" should Ġnot Ġhappen ") ĊĠĠĠĠĠĠĠĠĠĠĠ ĠB tor . Status . SAT Ġ-> ĠResult . Sat Result ( collect Model ( ctx , Ġstate )) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġcheck ( state : ĠBool _, Ġquery : ĠBool _ ): ĠB tor . Status Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġ( state _, Ġquery _) Ġ= Ġstate Ġto Ġquery ĊĊĠĠĠĠĠĠĠ Ġstate _. as Ax iom (). assert Form () ĊĠĠĠĠĠĠĠ Ġef . build Subtype Ax iom s ( tf ). as Ax iom (). assert Form () ĊĠĠĠĠĠĠĠ Ġquery _. axi om . assert Form () ĊĠĠĠĠĠĠĠ Ġquery _. expr . assert Form () ĊĊĠĠĠĠĠĠĠ Ġif Ġ( log Form ul ae ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġlog . debug ( ef . ctx . dump S mt 2 ()) ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġlog . debug (" Running ĠB oo lect or Ġsolver ") ĊĠĠĠĠĠĠĠ Ġval Ġresult Ġ= Ġef . ctx . check () Ġ?: Ġunreachable Ġ{ Ġlog . error (" Solver Ġerror ") Ġ} ĊĊĠĠĠĠĠĠĠ Ġlog . debug (" Solver Ġfinished ") ĊĊĠĠĠĠĠĠĠ Ġreturn Ġresult ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun ĠB oo lect or Context . recover Property ( ĊĠĠĠĠĠĠĠ Ġptr : ĠTerm , ĊĠĠĠĠĠĠĠ Ġmem space : ĠInt , ĊĠĠĠĠĠĠĠ Ġtype : ĠK ex Type , ĊĠĠĠĠĠĠĠ Ġname : ĠString ĊĠĠĠ Ġ): ĠPair < Term , ĠTerm > Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġptr Expr Ġ= ĠB oo lect or Converter ( tf ). convert ( ptr , Ġef , Ġthis ) Ġas ? ĠPtr _ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ?: Ġunreachable Ġ{ Ġlog . error (" Non - ptr Ġexpr Ġfor Ġpointer Ġ$ ptr ") Ġ} ĊĠĠĠĠĠĠĠ Ġval Ġstart Prop Ġ= Ġget Initial Properties ( mem space , Ġname ) ĊĠĠĠĠĠĠĠ Ġval Ġend Prop Ġ= Ġget Properties ( mem space , Ġname ) ĊĊĠĠĠĠĠĠĠ Ġval Ġstart V Ġ= Ġstart Prop . load ( ptr Expr , ĠB oo lect or Expr Factory . getType Size ( type ). int ) ĊĠĠĠĠĠĠĠ Ġval Ġend V Ġ= Ġend Prop . load ( ptr Expr , ĠB oo lect or Expr Factory . getType Size ( type ). int ) ĊĊĠĠĠĠĠĠĠ Ġval Ġmodel Start V Ġ= ĠB oo lect or Un logic . undo ( start V . expr ) ĊĠĠĠĠĠĠĠ Ġval Ġmodel End V Ġ= ĠB oo lect or Un logic . undo ( end V . expr ) ĊĠĠĠĠĠĠĠ Ġreturn Ġmodel Start V Ġto Ġmodel End V ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun ĠMutable Map < Int , ĠMutable Map < String , ĠMemory Pair >> . recover Property ( ĊĠĠĠĠĠĠĠ Ġctx : ĠB oo lect or Context , ĊĠĠĠĠĠĠĠ Ġptr : ĠTerm , ĊĠĠĠĠĠĠĠ Ġmem space : ĠInt , ĊĠĠĠĠĠĠĠ Ġtype : ĠK ex Type , ĊĠĠĠĠĠĠĠ Ġname : ĠString ĊĠĠĠ Ġ) Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġptr Expr Ġ= ĠB oo lect or Converter ( tf ). convert ( ptr , Ġef , Ġctx ) Ġas ? ĠPtr _ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ?: Ġunreachable Ġ{ Ġlog . error (" Non - ptr Ġexpr Ġfor Ġpointer Ġ$ ptr ") Ġ} ĊĠĠĠĠĠĠĠ Ġval Ġmodel Ptr Ġ= ĠB oo lect or Un logic . undo ( ptr Expr . expr ) ĊĊĠĠĠĠĠĠĠ Ġval Ġ( model Start T , Ġmodel End T ) Ġ= Ġctx . recover Property ( ptr , Ġmem space , Ġtype , Ġname ) ĊĠĠĠĠĠĠĠ Ġval Ġtype Pair Ġ= Ġthis . get Or Put ( mem space , Ġ:: hash Map Of ). get Or Put ( name ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġhash Map Of < Term , ĠTerm >() Ġto Ġhash Map Of () ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġtype Pair . first [ model Ptr ] Ġ= Ġmodel Start T ĊĠĠĠĠĠĠĠ Ġtype Pair . second [ model Ptr ] Ġ= Ġmodel End T ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġprivate Ġfun Ġcollect Model ( ctx : ĠB oo lect or Context , Ġvar arg Ġstates : ĠPredicate State ): ĠS MT Model Ġ{ ĊĠĠĠĠĠĠĠ Ġval Ġ( ptr s , Ġvars ) Ġ= Ġstates . fold ( set Of < Term >() Ġto Ġset Of < Term >()) Ġ{ Ġacc , Ġps Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠ Ġacc . first Ġ+ Ġcollect Pointers ( ps ) Ġto Ġacc . second Ġ+ Ġcollect Variables ( ps ) ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġval Ġassignments Ġ= Ġvars . associate With Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġexpr Ġ= ĠB oo lect or Converter ( tf ). convert ( it , Ġef , Ġctx ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġb oo lect or Expr Ġ= Ġexpr . expr ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġ// Ġthis Ġis Ġneeded Ġbecause Ġb oo lect or Ġrepresents Ġreal Ġnumbers Ġas Ġintegers ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġund one Ġ= ĠB oo lect or Un logic . undo ( b oo lect or Expr ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġactual Value Ġ= Ġwhen Ġ( it . type ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠK ex Real Ġ-> Ġwhen Ġ( und one ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠConst Int Term Ġ-> Ġterm Ġ{ Ġconst ( und one . value . toFloat ()) Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠConst Long Term Ġ-> Ġterm Ġ{ Ġconst ( und one . value . toDouble ()) Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġunreachable Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġlog . error (" Unexpected Ġintegral Ġterm Ġwhen Ġtrying Ġto Ġre animate Ġfloating Ġpoint Ġvalue : Ġ$ und one ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġund one ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġactual Value ĊĠĠĠĠĠĠĠ Ġ}. to Mutable Map () ĊĊĠĠĠĠĠĠĠ Ġval Ġmem ories Ġ= Ġhash Map Of < Int , ĠPair < Mutable Map < Term , ĠTerm >, ĠMutable Map < Term , ĠTerm >> >() ĊĠĠĠĠĠĠĠ Ġval Ġproperties Ġ= Ġhash Map Of < Int , ĠMutable Map < String , ĠPair < Mutable Map < Term , ĠTerm >, ĠMutable Map < Term , ĠTerm >>>> () ĊĠĠĠĠĠĠĠ Ġval Ġtype Map Ġ= Ġhash Map Of < Term , ĠK ex Type >() ĊĊĠĠĠĠĠĠĠ Ġfor Ġ(( type , Ġvalue ) Ġin Ġef . type Map ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġactual Value Ġ= ĠB oo lect or Un logic . undo ( value . expr ) ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtype Map [ actual Value ] Ġ= Ġtype ĊĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠ Ġfor Ġ( ptr Ġin Ġptr s ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġmem space Ġ= Ġptr . mem space ĊĊĠĠĠĠĠĠĠĠĠĠĠ Ġwhen Ġ( ptr ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠField Load Term Ġ-> Ġ{} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġis ĠField Term Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġname Ġ= Ġ"${ ptr . klass }.${ ptr . fieldName String }" ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġproperties . recover Property ( ctx , Ġptr . owner , Ġmem space , Ġ( ptr . type Ġas ĠK ex Reference ). reference , Ġname ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġproperties . recover Property ( ctx , Ġptr . owner , Ġmem space , Ġptr . type , Ġ" type ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġelse Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġstart Mem Ġ= Ġctx . get Initial Memory ( mem space ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġend Mem Ġ= Ġctx . get Memory ( mem space ) ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġptr Expr Ġ= ĠB oo lect or Converter ( tf ). convert ( ptr , Ġef , Ġctx ) Ġas ? ĠPtr _ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ?: Ġunreachable Ġ{ Ġlog . error (" Non - ptr Ġexpr Ġfor Ġpointer Ġ$ ptr ") Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġstart V Ġ= Ġstart Mem . load ( ptr Expr , ĠB oo lect or Expr Factory . getType Size ( ptr . type ). int ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġend V Ġ= Ġend Mem . load ( ptr Expr , ĠB oo lect or Expr Factory . getType Size ( ptr . type ). int ) ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġmodel Ptr Ġ= ĠB oo lect or Un logic . undo ( ptr Expr . expr ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġmodel Start V Ġ= ĠB oo lect or Un logic . undo ( start V . expr ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġval Ġmodel End V Ġ= ĠB oo lect or Un logic . undo ( end V . expr ) ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġmem ories . get Or Put ( mem space ) Ġ{ Ġhash Map Of < Term , ĠTerm >() Ġto Ġhash Map Of () Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġmem ories . getValue ( mem space ). first [ model Ptr ] Ġ= Ġmodel Start V ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġmem ories . getValue ( mem space ). second [ model Ptr ] Ġ= Ġmodel End V ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġproperties . recover Property ( ctx , Ġptr , Ġmem space , Ġptr . type , Ġ" type ") ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġif Ġ( ptr . type Ġis ĠK ex Array ) Ġ{ ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġproperties . recover Property ( ctx , Ġptr , Ġmem space , ĠK ex Int (), Ġ" length ") ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġkt assert ( assignments . get Or Put ( ptr ) Ġ{ Ġmodel Ptr Ġ} Ġ== Ġmodel Ptr ) ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġreturn ĠS MT Model ( ĊĠĠĠĠĠĠĠĠĠĠĠ Ġassignments , ĊĠĠĠĠĠĠĠĠĠĠĠ Ġmem ories . map Ġ{ Ġ( mem space , Ġpair ) Ġ-> Ġmem space Ġto ĠMemory Shape ( pair . first , Ġpair . second ) Ġ}. toMap (), ĊĠĠĠĠĠĠĠĠĠĠĠ Ġproperties . map Ġ{ Ġ( mem space , Ġnames ) Ġ-> ĊĠĠĠĠĠĠĠĠĠĠĠĠĠĠĠ Ġmem space Ġto Ġnames . map Ġ{ Ġ( name , Ġpair ) Ġ-> Ġname Ġto ĠMemory Shape ( pair . first , Ġpair . second ) Ġ}. toMap () ĊĠĠĠĠĠĠĠĠĠĠĠ Ġ}. toMap (), ĊĠĠĠĠĠĠĠĠĠĠĠ Ġtype Map ĊĠĠĠĠĠĠĠ Ġ) ĊĠĠĠ Ġ} ĊĊĠĠĠ Ġoverride Ġfun Ġclose () Ġ= Ġef . ctx . release () Ċ } Ċ