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:
- 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.
- Alphabetic
- By Inheritance
- Semantics
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- All
Instance Constructors
- new Semantics()(implicit arg0: Expression[Exp], arg1: JoinLattice[Abs], arg2: Address[Addr], arg3: Timestamp[Time])
Abstract Value Members
-
abstract
def
parse(program: String): Exp
Defines how to parse a program
-
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
-
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
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
- def +(other: String): String
- def ->[B](y: B): (Semantics[Exp, Abs, Addr, Time], B)
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- implicit def actionToSet(action: Action[Exp, Abs, Addr]): Set[Action[Exp, Abs, Addr]]
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
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
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate() @throws( ... )
- def ensuring(cond: (Semantics[Exp, Abs, Addr, Time]) ⇒ Boolean, msg: ⇒ Any): Semantics[Exp, Abs, Addr, Time]
- def ensuring(cond: (Semantics[Exp, Abs, Addr, Time]) ⇒ Boolean): Semantics[Exp, Abs, Addr, Time]
- def ensuring(cond: Boolean, msg: ⇒ Any): Semantics[Exp, Abs, Addr, Time]
- def ensuring(cond: Boolean): Semantics[Exp, Abs, Addr, Time]
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def formatted(fmtstr: String): String
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
def
initialBindings: Iterable[(String, Addr, Abs)]
Defines the elements in the initial environment/store
- def initialEnv: Iterable[(String, Addr)]
- def initialStore: Iterable[(Addr, Abs)]
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- implicit def mfActionToActions(mf: MayFail[Action[Exp, Abs, Addr]]): Set[Action[Exp, Abs, Addr]]
- implicit def mfToActions(mf: MayFail[Set[Action[Exp, Abs, Addr]]]): Set[Action[Exp, Abs, Addr]]
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
-
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
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
- def →[B](y: B): (Semantics[Exp, Abs, Addr, Time], B)
- object Action extends ActionHelpers[Exp, Abs, Addr]