Skip to content

Commit

Permalink
basic framework for BTA
Browse files Browse the repository at this point in the history
  • Loading branch information
jhnaldo committed Feb 5, 2025
1 parent 652d951 commit 51a0e94
Show file tree
Hide file tree
Showing 9 changed files with 211 additions and 15 deletions.
3 changes: 0 additions & 3 deletions src/main/scala/esmeta/analyzer/Analyzer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,6 @@ abstract class Analyzer
/** check reachability of return points */
def reachable(rp: ReturnPoint): Boolean

/** symbolic types */
type SymTy <: SymTyLike

/** abstract states */
type AbsState <: AbsStateLike

Expand Down
11 changes: 0 additions & 11 deletions src/main/scala/esmeta/analyzer/DomainLike.scala
Original file line number Diff line number Diff line change
Expand Up @@ -27,17 +27,6 @@ trait DomainLikeDecl { self: Analyzer =>
override def toString: String = stringify(this)(using domain.rule)
}

/** Symbolic types */
trait SymTyLike extends DomainElemLike[SymTy] { self: SymTy =>

/** abstract domain */
def domain = SymTy

/** get string of symbolic type */
def getString: String
}
val SymTy: DomainLike[SymTy]

/** abstract values */
trait AbsValueLike extends DomainElemLike[AbsValue] { self: AbsValue =>

Expand Down
22 changes: 22 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/AbsRet.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
package esmeta.analyzer.bta

import esmeta.util.Appender.*

/** abstract return values */
trait AbsRetDecl { self: BindingTimeAnalyzer =>
case class AbsRet(value: AbsValue) extends AbsRetLike {
/** has imprecise elements */
def hasImprec: Boolean = ???
}
object AbsRet extends DomainLike[AbsRet] {

/** top element */
def Top: AbsRet = ???

/** bottom element */
def Bot: AbsRet = ???

/** appender */
given rule: Rule[AbsRet] = ???
}
}
27 changes: 27 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/AbsState.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
package esmeta.analyzer.bta

import esmeta.ir.*
import esmeta.util.Appender.*

/** abstract states */
trait AbsStateDecl { self: BindingTimeAnalyzer =>
case class AbsState(
map: Map[Local, BindingTime]
) extends AbsStateLike {
/** has imprecise elements */
def hasImprec: Boolean = ???
}
object AbsState extends DomainLike[AbsState] {

/** top element */
def Top: AbsState = ???

/** bottom element */
def Bot: AbsState = ???

/** appender */
given rule: Rule[AbsState] = ???
}

enum BindingTime { case Static, Dynamic }
}
65 changes: 65 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/AbsTransfer.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
package esmeta.analyzer.bta

import esmeta.cfg.{util => _, *}
import esmeta.ir.{Func => _, util => _, *}
import esmeta.state.*
import esmeta.ty.*
import esmeta.util.*
import esmeta.util.BaseUtils.*
import scala.annotation.tailrec
import esmeta.es.builtin.JOB_QUEUE

trait AbsTransferDecl { analyzer: BindingTimeAnalyzer =>

/** abstract transfer function */
class AbsTransfer extends AbsTransferLike {

/** loading monads */
import monad.*

/** transfer function for node points */
def apply(np: NodePoint[_]): Unit = ???

/** transfer function for return points */
def apply(rp: ReturnPoint): Unit = ???

/** transfer function for normal instructions */
def transfer(
inst: NormalInst,
)(using np: NodePoint[_]): Updater = ???

/** transfer function for expressions */
def transfer(
expr: Expr,
)(using np: NodePoint[Node]): Result[AbsValue] = ???

/** transfer function for unary operators */
def transfer(
st: AbsState,
unary: EUnary,
operand: AbsValue,
)(using np: NodePoint[Node]): AbsValue = ???

/** transfer function for binary operators */
def transfer(
st: AbsState,
binary: EBinary,
left: AbsValue,
right: AbsValue,
)(using np: NodePoint[Node]): AbsValue = ???

/** transfer for variadic operators */
def transfer(
st: AbsState,
vop: VOp,
vs: List[AbsValue],
)(using np: NodePoint[Node]): AbsValue = ???

/** transfer for mathematical operators */
def transfer(
st: AbsState,
mop: MOp,
vs: List[AbsValue],
)(using np: NodePoint[Node]): AbsValue = ???
}
}
25 changes: 25 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/AbsValue.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
package esmeta.analyzer.bta

import esmeta.util.Appender.*

/** abstract values */
trait AbsValueDecl { self: BindingTimeAnalyzer =>
case class AbsValue() extends AbsValueLike {
/** has imprecise elements */
def hasImprec: Boolean = ???

/** get string of abstract value with an abstract state */
def getString(state: AbsState): String = ???
}
object AbsValue extends DomainLike[AbsValue] {

/** top element */
def Top: AbsValue = ???

/** bottom element */
def Bot: AbsValue = ???

/** appender */
given rule: Rule[AbsValue] = ???
}
}
46 changes: 46 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/BindingTimeAnalyzer.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
package esmeta.analyzer.bta

import esmeta.{ANALYZE_LOG_DIR, LINE_SEP}
import esmeta.analyzer.*
import esmeta.cfg.*
import esmeta.es.*
import esmeta.ir.{Func => _, *, given}
import esmeta.util.*
import esmeta.util.Appender.*
import esmeta.util.BaseUtils.*
import esmeta.util.SystemUtils.*

/** specification type analyzer for ECMA-262 */
class BindingTimeAnalyzer(
val cfg: CFG
) extends Analyzer
with AbsValueDecl
with AbsStateDecl
with AbsRetDecl
with ViewDecl {

/** worklist of control points */
val worklist: Worklist[ControlPoint] = ???

/** abstract transfer function */
type AbsTransfer <: AbsTransferLike
val transfer: AbsTransfer = ???

/** check reachability of node points */
def reachable(np: NodePoint[Node]): Boolean = ???

/** check reachability of return points */
def reachable(rp: ReturnPoint): Boolean = ???

/** get string for result of control points */
def getString(
cp: ControlPoint,
color: Option[String] = None,
detail: Boolean = false,
): String = ???

val log: Boolean = ???

/** logging the current analysis result */
def logging: Unit = ???
}
25 changes: 25 additions & 0 deletions src/main/scala/esmeta/analyzer/bta/View.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
package esmeta.analyzer.bta

import esmeta.ty.*
import esmeta.ty.util.{Stringifier => TyStringifier}
import esmeta.util.Appender.*

/** view abstraction */
trait ViewDecl { self: BindingTimeAnalyzer =>

/** view abstraction for analysis sensitivities */
case class View() extends ViewLike {

/** empty check */
def isEmpty: Boolean = ???
}

/** appender */
def viewRule(detail: Boolean): Rule[View] = (app, view) => ???

/** empty view */
val emptyView: View = View()

/** get entry views of loops */
def getEntryView(view: View): View = view
}
2 changes: 1 addition & 1 deletion src/main/scala/esmeta/analyzer/tychecker/SymTy.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import esmeta.util.Appender.*
import esmeta.util.BaseUtils.*

trait SymTyDecl { self: TyChecker =>
enum SymTy extends SymTyLike {
enum SymTy {
case STy(ty: ValueTy)
case SRef(ref: SymRef)
case SNormal(symty: SymTy)
Expand Down

0 comments on commit 51a0e94

Please sign in to comment.