Packages

  • package root
    Definition Classes
    root
  • abstract class Semantics[Exp, Abs, Addr, Time] extends AnyRef

    This is where the interface of a language's semantics is defined.

    This is where the interface of a language's semantics is defined. By defining the semantics of a language, you get an abstract abstract machine for free (but you might need to adapt existing lattices to support values from your language).

    Semantics should be defined as small-step operational semantics. To define a semantics, you have to implement the Semantics trait. You'll need to specialize it on the type of expression of your language (e.g., for ANF, ANFSemantics specializes on ANFExp). To do so, you need to define what actions should be taken when:

    1. Evaluating an expression e (stepEval) 2. Continuing evaluation when a value v has been reached (stepKont)

    To have a simple overview of how semantics should be defined, look at the ANFSemantics.scala, as it defines semantics of ANF Scheme, a very lightweight language. A more complex definition resides in SchemeSemantics.scala.

    Definition Classes
    root
c

Semantics

abstract class Semantics[Exp, Abs, Addr, Time] extends AnyRef

This is where the interface of a language's semantics is defined. By defining the semantics of a language, you get an abstract abstract machine for free (but you might need to adapt existing lattices to support values from your language).

Semantics should be defined as small-step operational semantics. To define a semantics, you have to implement the Semantics trait. You'll need to specialize it on the type of expression of your language (e.g., for ANF, ANFSemantics specializes on ANFExp). To do so, you need to define what actions should be taken when:

  1. Evaluating an expression e (stepEval) 2. Continuing evaluation when a value v has been reached (stepKont)

To have a simple overview of how semantics should be defined, look at the ANFSemantics.scala, as it defines semantics of ANF Scheme, a very lightweight language. A more complex definition resides in SchemeSemantics.scala.

Linear Supertypes
AnyRef, Any
Known Subclasses
ANFSemantics, ASchemeSemantics, ASchemeSemanticsWithVisitorAndOptimization, BaseSchemeSemantics, CSchemeSemantics, DotSemantics, LamSemantics, SchemeSemantics, SemanticsWithAnalysis
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Semantics
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Semantics()(implicit arg0: Expression[Exp], arg1: JoinLattice[Abs], arg2: Address[Addr], arg3: Timestamp[Time])

Abstract Value Members

  1. abstract def parse(program: String): Exp

    Defines how to parse a program

  2. abstract def stepEval(e: Exp, env: Environment[Addr], store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    Defines what actions should be taken when an expression e needs to be evaluated, in environment env with store store

  3. abstract def stepKont(v: Abs, frame: Frame, store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    Defines what actions should be taken when a value v has been reached, and the topmost frame is frame

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def +(other: String): String
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to any2stringadd[Semantics[Exp, Abs, Addr, Time]] performed by method any2stringadd in scala.Predef.
    Definition Classes
    any2stringadd
  4. def ->[B](y: B): (Semantics[Exp, Abs, Addr, Time], B)
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to ArrowAssoc[Semantics[Exp, Abs, Addr, Time]] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
    Annotations
    @inline()
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. implicit def actionToSet(action: Action[Exp, Abs, Addr]): Set[Action[Exp, Abs, Addr]]
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def bindArgs(l: List[(Identifier, Abs)], env: Environment[Addr], store: Store[Addr, Abs], t: Time): (Environment[Addr], Store[Addr, Abs])

    Binds arguments in the environment and store.

    Binds arguments in the environment and store. Arguments are given as a list of triple, where each triple is made of:

    • the name of the argument
    • the position of the argument
    • the value of the argument
    Attributes
    protected
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate() @throws( ... )
  10. def ensuring(cond: (Semantics[Exp, Abs, Addr, Time]) ⇒ Boolean, msg: ⇒ Any): Semantics[Exp, Abs, Addr, Time]
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to Ensuring[Semantics[Exp, Abs, Addr, Time]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  11. def ensuring(cond: (Semantics[Exp, Abs, Addr, Time]) ⇒ Boolean): Semantics[Exp, Abs, Addr, Time]
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to Ensuring[Semantics[Exp, Abs, Addr, Time]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  12. def ensuring(cond: Boolean, msg: ⇒ Any): Semantics[Exp, Abs, Addr, Time]
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to Ensuring[Semantics[Exp, Abs, Addr, Time]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  13. def ensuring(cond: Boolean): Semantics[Exp, Abs, Addr, Time]
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to Ensuring[Semantics[Exp, Abs, Addr, Time]] performed by method Ensuring in scala.Predef.
    Definition Classes
    Ensuring
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. def formatted(fmtstr: String): String
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to StringFormat[Semantics[Exp, Abs, Addr, Time]] performed by method StringFormat in scala.Predef.
    Definition Classes
    StringFormat
    Annotations
    @inline()
  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  19. def initialBindings: Iterable[(String, Addr, Abs)]

    Defines the elements in the initial environment/store

  20. def initialEnv: Iterable[(String, Addr)]
  21. def initialStore: Iterable[(Addr, Abs)]
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. implicit def mfActionToActions(mf: MayFail[Action[Exp, Abs, Addr]]): Set[Action[Exp, Abs, Addr]]
  24. implicit def mfToActions(mf: MayFail[Set[Action[Exp, Abs, Addr]]]): Set[Action[Exp, Abs, Addr]]
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  28. def stepReceive(self: Any, mname: String, margsv: List[Abs], d: Exp, env: Environment[Addr], store: Store[Addr, Abs], t: Time): Set[Action[Exp, Abs, Addr]]

    WIP

  29. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  30. def toString(): String
    Definition Classes
    AnyRef → Any
  31. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  32. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  33. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  34. def →[B](y: B): (Semantics[Exp, Abs, Addr, Time], B)
    Implicit
    This member is added by an implicit conversion from Semantics[Exp, Abs, Addr, Time] to ArrowAssoc[Semantics[Exp, Abs, Addr, Time]] performed by method ArrowAssoc in scala.Predef.
    Definition Classes
    ArrowAssoc
  35. object Action extends ActionHelpers[Exp, Abs, Addr]

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Inherited by implicit conversion any2stringadd from Semantics[Exp, Abs, Addr, Time] to any2stringadd[Semantics[Exp, Abs, Addr, Time]]

Inherited by implicit conversion StringFormat from Semantics[Exp, Abs, Addr, Time] to StringFormat[Semantics[Exp, Abs, Addr, Time]]

Inherited by implicit conversion Ensuring from Semantics[Exp, Abs, Addr, Time] to Ensuring[Semantics[Exp, Abs, Addr, Time]]

Inherited by implicit conversion ArrowAssoc from Semantics[Exp, Abs, Addr, Time] to ArrowAssoc[Semantics[Exp, Abs, Addr, Time]]

Ungrouped