root package
package root
- Alphabetic
- Public
- All
Type Members
-
class
AAM[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]
Implementation of a CESK machine following the AAM approach (Van Horn, David, and Matthew Might.
-
class
AAMAACP4F[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]
AAM/AAC/P4F techniques combined in a single machine abstraction
-
class
AAMNS[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]
Copy of AAM machine but without the subsumption part (AAMNS - AAM No Subsumption).
Copy of AAM machine but without the subsumption part (AAMNS - AAM No Subsumption). Use as comparison to Scala-Par-AM https://bitbucket.org/OPiMedia/scala-par-am (a parallel version of Scala-AM).
- trait ANFAtomicExp extends ANFExp
-
trait
ANFExp extends AnyRef
Abstract syntax of ANF programs
- case class ANFFuncall(f: ANFAtomicExp, args: List[ANFAtomicExp], pos: Position) extends ANFExp with Product with Serializable
- case class ANFIf(cond: ANFAtomicExp, cons: ANFExp, alt: ANFExp, pos: Position) extends ANFExp with Product with Serializable
- case class ANFLambda(args: List[Identifier], body: ANFExp, pos: Position) extends ANFAtomicExp with Product with Serializable
- case class ANFLet(variable: Identifier, value: ANFExp, body: ANFExp, pos: Position) extends ANFExp with Product with Serializable
- case class ANFLetrec(variable: Identifier, value: ANFExp, body: ANFExp, pos: Position) extends ANFExp with Product with Serializable
- case class ANFQuoted(quoted: SExp, pos: Position) extends ANFExp with Product with Serializable
-
class
ANFSemantics[Abs, Addr, Time] extends Semantics[ANFExp, Abs, Addr, Time]
Semantics for ANF Scheme (abstract grammar defined in ANF.scala)
- case class ANFSet(variable: Identifier, value: ANFAtomicExp, pos: Position) extends ANFExp with Product with Serializable
- case class ANFValue(value: Value, pos: Position) extends ANFAtomicExp with Product with Serializable
- case class ANFVar(v: Identifier) extends ANFAtomicExp with Product with Serializable
- trait ASchemeLattice extends SchemeLattice
- class ASchemeSemantics[Abs, Addr, Time, PID] extends SchemeSemantics[Abs, Addr, Time]
- class ASchemeSemanticsWithVisitorAndOptimization[Abs, Addr, Time, PID] extends ASchemeSemantics[Abs, Addr, Time, PID]
-
abstract
class
AbstractMachine[Exp, Abs, Addr, Time] extends AnyRef
The interface of the abstract machine itself.
The interface of the abstract machine itself. The abstract machine is parameterized by abstract values, addresses and expressions. Look into AAM.scala for an example of how to define these parameters
-
abstract
class
Action[Exp, Abs, Addr] extends AnyRef
The different kinds of actions that can be taken by the abstract machine
-
case class
ActionError[Exp, Abs, Addr](error: SemanticError)(implicit evidence$43: Expression[Exp], evidence$44: JoinLattice[Abs], evidence$45: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
An error has been reached
-
case class
ActionEval[Exp, Abs, Addr](e: Exp, env: Environment[Addr], store: Store[Addr, Abs], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$37: Expression[Exp], evidence$38: JoinLattice[Abs], evidence$39: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
Evaluation continues with expression e in environment env
- class ActionHelpers[Exp, Abs, Addr] extends AnyRef
-
case class
ActionJoin[TID, Exp, Abs, Addr](t: TID, store: Store[Addr, Abs], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$50: ThreadIdentifier[TID], evidence$51: Expression[Exp], evidence$52: JoinLattice[Abs], evidence$53: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
Waits for the execution of a thread, with tid as its identifier.
-
case class
ActionPush[Exp, Abs, Addr](frame: Frame, e: Exp, env: Environment[Addr], store: Store[Addr, Abs], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$34: Expression[Exp], evidence$35: JoinLattice[Abs], evidence$36: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
A frame needs to be pushed on the stack, and the interpretation continues by evaluating expression e in environment env
-
case class
ActionReachedValue[Exp, Abs, Addr](v: Abs, store: Store[Addr, Abs], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$31: Expression[Exp], evidence$32: JoinLattice[Abs], evidence$33: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
A value is reached by the interpreter.
A value is reached by the interpreter. As a result, a continuation will be popped with the given reached value.
-
case class
ActionSpawn[TID, Exp, Abs, Addr](t: TID, e: Exp, env: Environment[Addr], store: Store[Addr, Abs], act: Action[Exp, Abs, Addr], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$46: ThreadIdentifier[TID], evidence$47: Expression[Exp], evidence$48: JoinLattice[Abs], evidence$49: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
Spawns a new thread that evaluates expression e in environment ρ.
Spawns a new thread that evaluates expression e in environment ρ. The current thread continues its execution by performing action act.
-
case class
ActionStepIn[Exp, Abs, Addr](fexp: Exp, clo: (Exp, Environment[Addr]), e: Exp, env: Environment[Addr], store: Store[Addr, Abs], argsv: List[(Exp, Abs)], effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$40: Expression[Exp], evidence$41: JoinLattice[Abs], evidence$42: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
Similar to ActionEval, but only used when stepping inside a function's body (clo is therefore the function stepped into).
Similar to ActionEval, but only used when stepping inside a function's body (clo is therefore the function stepped into). The expressions and values of the arguments should also be provided, as they can be needed by the abstract machine.
- case class ActorActionBecome[Exp, Abs, Addr, Time, PID](name: String, actd: Exp, env: Environment[Addr], store: Store[Addr, Abs], vres: Abs, effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$68: Expression[Exp], evidence$69: JoinLattice[Abs], evidence$70: Address[Addr], evidence$71: Timestamp[Time], evidence$72: ThreadIdentifier[PID]) extends Action[Exp, Abs, Addr] with Product with Serializable
- case class ActorActionCreate[Exp, Abs, Addr, Time, PID](name: String, actd: Exp, e: Exp, env: Environment[Addr], store: Store[Addr, Abs], fres: (PID) ⇒ Abs, effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$63: Expression[Exp], evidence$64: JoinLattice[Abs], evidence$65: Address[Addr], evidence$66: Timestamp[Time], evidence$67: ThreadIdentifier[PID]) extends Action[Exp, Abs, Addr] with Product with Serializable
- class ActorActionHelpers[Exp, Abs, Addr, Time, PID] extends AnyRef
- case class ActorActionSend[PID, Exp, Abs, Addr](p: PID, name: String, msg: List[Abs], vres: Abs, effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$59: ThreadIdentifier[PID], evidence$60: Expression[Exp], evidence$61: JoinLattice[Abs], evidence$62: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
- case class ActorActionTerminate[Exp, Abs, Addr](effects: Set[Effect[Addr]] = Set[Effect[Addr]]())(implicit evidence$73: Expression[Exp], evidence$74: JoinLattice[Abs], evidence$75: Address[Addr]) extends Action[Exp, Abs, Addr] with Product with Serializable
- trait ActorTimestamp[T] extends Timestamp[T]
- trait ActorTimestampWrapper extends TimestampWrapper
- abstract class ActorVisitor[Exp, Abs, Addr] extends AnyRef
- class ActorsAAM[Exp, Abs, Addr, Time, PID] extends AbstractMachine[Exp, Abs, Addr, Time]
- class ActorsAAMGlobalStore[Exp, Abs, Addr, Time, PID] extends AbstractMachine[Exp, Abs, Addr, Time]
- trait Address[A] extends AnyRef
- trait AddressWrapper extends AnyRef
- abstract class Analysis[L, Exp, Abs, Addr, Time] extends AnyRef
-
case class
App(e1: LamExp, e2: LamExp, pos: Position) extends LamExp with Product with Serializable
An application: (e1 e2)
- case class ArityError(name: String, expected: Int, got: Int) extends SemanticError with Product with Serializable
-
class
BaseSchemeSemantics[V, Addr, Time] extends Semantics[SchemeExp, V, Addr, Time]
Basic Scheme semantics, without any optimization
-
case class
BasicEnvironment[Addr](content: Map[String, Addr])(implicit evidence$2: Address[Addr]) extends Environment[Addr] with Product with Serializable
Basic mapping from names to addresses
- case class BasicKontStore[KontAddr](content: Map[KontAddr, Set[Kont[KontAddr]]])(implicit evidence$3: KontAddress[KontAddr]) extends KontStore[KontAddr] with Product with Serializable
-
case class
BasicStore[Addr, Abs](content: Map[Addr, Abs])(implicit evidence$3: Address[Addr], evidence$4: JoinLattice[Abs]) extends Store[Addr, Abs] with Product with Serializable
Basic store with no fancy feature, just a map from addresses to values
- abstract class Benchmarks extends AnyRef
-
trait
BoolLattice[B] extends LatticeElement[B]
A lattice for booleans
- class BoundedInteger extends AnyRef
- case class BoundedListMboxImpl[PID, Abs](bound: Int) extends MboxImpl[PID, Abs] with Product with Serializable
- case class BoundedMultisetMboxImpl[PID, Abs](bound: Int) extends MboxImpl[PID, Abs] with Product with Serializable
- trait CSchemeLattice extends SchemeLattice
- class CSchemePrimitives[Addr, Abs] extends SchemePrimitives[Addr, Abs]
- class CSchemeSemantics[Abs, Addr, Time, TID] extends SchemeSemantics[Abs, Addr, Time]
- case class CannotAccessCar(v: String) extends SemanticError with Product with Serializable
- case class CannotAccessCdr(v: String) extends SemanticError with Product with Serializable
- case class CannotAccessVector(vector: String) extends SemanticError with Product with Serializable
-
sealed
trait
Cardinality extends AnyRef
Cardinality represents how much information a lattice value represents
- case class CardinalityNumber(n: Int) extends Cardinality with Product with Serializable
-
trait
CharLattice[C] extends LatticeElement[C]
A lattice for characters
- case class Color(hex: String) extends Product with Serializable
-
case class
CombinedEnvironment[Addr](ro: Environment[Addr], w: Environment[Addr])(implicit evidence$3: Address[Addr]) extends Environment[Addr] with Product with Serializable
Environment that combines a default read-only environment with a writable environment
-
case class
CombinedStore[Addr, Abs](ro: Store[Addr, Abs], w: Store[Addr, Abs])(implicit evidence$5: Address[Addr], evidence$6: JoinLattice[Abs]) extends Store[Addr, Abs] with Product with Serializable
Store that combines a default read-only store with a writable store
-
class
ConcreteMachine[Exp, Abs, Addr, Time] extends EvalKontMachine[Exp, Abs, Addr, Time]
Implementation of a concrete CESK machine.
Implementation of a concrete CESK machine. It should be faster than other implementations in this framework because it doesn't store the set of visited states.
- class ConcurrentAAM[Exp, Abs, Addr, Time, TID] extends AbstractMachine[Exp, Abs, Addr, Time]
- trait ContextSensitiveTID extends AnyRef
- trait Count extends AnyRef
- case class CountingMap[A, B](content: Map[A, (Count, Set[B])]) extends Product with Serializable
- case class CountingStore[Addr, Abs](content: Map[Addr, (Count, Abs)])(implicit evidence$11: Address[Addr], evidence$12: JoinLattice[Abs]) extends Store[Addr, Abs] with Product with Serializable
-
case class
DeltaStore[Addr, Abs](content: Map[Addr, Abs], d: Map[Addr, Abs])(implicit evidence$7: Address[Addr], evidence$8: JoinLattice[Abs]) extends Store[Addr, Abs] with Product with Serializable
A store that supports store deltas.
A store that supports store deltas. Many operations are not implemented because they are not needed.
- class DotLanguage[Addr] extends AnyRef
- abstract class Effect[Addr] extends AnyRef
- case class EffectAcquire[Addr](target: Addr)(implicit evidence$21: Address[Addr]) extends Effect[Addr] with Product with Serializable
-
trait
EffectKind extends AnyRef
The different kinds of effects that can be generated by the semantics
- case class EffectReadConsCar[Addr](target: Addr)(implicit evidence$14: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectReadConsCdr[Addr](target: Addr)(implicit evidence$15: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectReadVariable[Addr](target: Addr)(implicit evidence$13: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectReadVector[Addr](target: Addr)(implicit evidence$16: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectRelease[Addr](target: Addr)(implicit evidence$22: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectWriteConsCar[Addr](target: Addr)(implicit evidence$18: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectWriteConsCdr[Addr](target: Addr)(implicit evidence$19: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectWriteVariable[Addr](target: Addr)(implicit evidence$17: Address[Addr]) extends Effect[Addr] with Product with Serializable
- case class EffectWriteVector[Addr](target: Addr)(implicit evidence$20: Address[Addr]) extends Effect[Addr] with Product with Serializable
- class EmptyActorVisitor[Exp, Abs, Addr] extends ActorVisitor[Exp, Abs, Addr]
- abstract class Environment[Addr] extends AnyRef
-
abstract
class
EvalKontMachine[Exp, Abs, Addr, Time] extends AbstractMachine[Exp, Abs, Addr, Time]
Abstract machine with a control component that works in an eval-kont way: it can either be evaluating something, or have reached a value and will pop a continuation.
- trait ExplorationType extends AnyRef
- trait Expression[E] extends AnyRef
- trait Frame extends AnyRef
-
class
Graph[N, A, C] extends AnyRef
Represents a graph where nodes are elements of N, and edges are annotated with elements of type-class GraphAnnotation
- trait GraphAnnotation[A, C] extends AnyRef
- case class GraphMboxImpl[PID, Abs]() extends MboxImpl[PID, Abs] with Product with Serializable
- trait GraphNode[N, C] extends AnyRef
- trait GraphOutput extends AnyRef
-
case class
Identifier(name: String, pos: Position) extends Product with Serializable
An identifier has a name and a position
- trait InsensitiveTID extends AnyRef
-
trait
IntLattice[I] extends LatticeElement[I]
A lattice for integers
-
trait
IsASchemeLattice[L] extends IsSchemeLattice[L]
A lattice for Actor Scheme
-
trait
IsCSchemeLattice[L] extends IsSchemeLattice[L]
A lattice for Concurrent Scheme
-
trait
IsSchemeLattice[L] extends JoinLattice[L]
A lattice for Scheme should support the following operations
- trait IsTaintLattice[L] extends IsSchemeLattice[L]
-
trait
JoinLattice[L] extends Monoid[L] with PartialOrdering[L]
A (join semi-)lattice L should support the following operations
- trait KAllocStrategy extends AnyRef
- case class KCFA(k: Int) extends TimestampWrapper with Product with Serializable
- case class KMessageTagSensitivity(k: Int) extends ActorTimestampWrapper with Product with Serializable
- class KeyMap[A] extends AnyRef
- case class Kont[KontAddr](frame: Frame, next: KontAddr)(implicit evidence$1: KontAddress[KontAddr]) extends Product with Serializable
- trait KontAddress[A] extends AnyRef
- abstract class KontStore[KontAddr] extends AnyRef
-
case class
Lam(x: Identifier, e: LamExp, pos: Position) extends LamExp with Product with Serializable
An abstraction: lambda x.
An abstraction: lambda x. e
-
trait
LamExp extends AnyRef
A lambda calculus expression is represented by a LamExp.
A lambda calculus expression is represented by a LamExp. It needs to have a position to identify its location in the input file.
-
trait
LamLattice[L] extends JoinLattice[L]
Our value domain should form a lattice, but we need support for a bit more than just join operations
-
class
LamSemantics[Abs, Addr, Time] extends Semantics[LamExp, Abs, Addr, Time]
This defines the semantics of call-by-value lambda expressions
-
trait
LatticeElement[L] extends Order[L] with Monoid[L] with Show[L]
We define here some domains that can will be useful to build a lattice for most languages.
- case class ListMboxImpl[PID, Abs]() extends MboxImpl[PID, Abs] with Product with Serializable
- case class MachineConfig(program: String, machine: Config.Machine.Value = Config.Machine.AAM, address: Config.Address.Value = Config.Address.Classical, lattice: Config.Lattice.Value = Config.Lattice.TypeSet, concrete: Boolean = false) extends Product with Serializable
- class MakeASchemeLattice[LSeq] extends ASchemeLattice
- class MakeCSchemeLattice[LSeq] extends CSchemeLattice
- class MakeSchemeLattice[S, B, I, F, C, Sym] extends SchemeLattice
- sealed trait MayFail[L] extends AnyRef
- case class MayFailBoth[L](l: L, errs: List[SemanticError]) extends MayFail[L] with Product with Serializable
- case class MayFailError[L](errs: List[SemanticError]) extends MayFail[L] with Product with Serializable
- case class MayFailSuccess[L](l: L) extends MayFail[L] with Product with Serializable
- case class MaybeTainted(sources: Set[Position]) extends TaintStatus with Product with Serializable
- trait MboxImpl[PID, Abs] extends AnyRef
- trait MboxSize extends AnyRef
- case class MboxSizeN(n: Int) extends MboxSize with Product with Serializable
- case class MessageNotSupported(actor: String, message: String, supported: List[String]) extends SemanticError with Product with Serializable
- case class MultisetMboxImpl[PID, Abs]() extends MboxImpl[PID, Abs] with Product with Serializable
- case class NotSupported(reason: String) extends SemanticError with Product with Serializable
- case class OperatorNotApplicable(name: String, arguments: List[String]) extends SemanticError with Product with Serializable
-
sealed
trait
Position extends AnyRef
This trait represents a position in a source file.
This trait represents a position in a source file. It's currently a wrapper around scala.util.parsing.input.Position, but will probably be updated in the future.
- case class PowersetMboxImpl[PID, Abs]() extends MboxImpl[PID, Abs] with Product with Serializable
-
trait
Primitive[Addr, Abs] extends AnyRef
Each primitive has to implement this trait.
- abstract class Primitives[Addr, Abs] extends AnyRef
- case class ProductAnalysis[L1, L2, Exp, Abs, Addr, Time](analysis1: Analysis[L1, Exp, Abs, Addr, Time], analysis2: Analysis[L2, Exp, Abs, Addr, Time])(implicit evidence$5: Expression[Exp], evidence$6: JoinLattice[Abs], evidence$7: Address[Addr], evidence$8: Timestamp[Time]) extends Analysis[(L1, L2), Exp, Abs, Addr, Time] with Product with Serializable
-
trait
RealLattice[F] extends LatticeElement[F]
A lattice for floats
- class RecordActorVisitor[Exp, Abs, Addr] extends ActorVisitor[Exp, Abs, Addr]
-
trait
SExp extends AnyRef
Abstract grammar elements for S-expressions include some positional information.
Abstract grammar elements for S-expressions include some positional information. This serves two purposes: identify where the s-expression resides in the input file, and as tagging information for the abstract machine.
-
case class
SExpId(id: Identifier) extends SExp with Product with Serializable
An identifier, such as foo, bar, etc.
- class SExpLexer extends Lexical with SExpTokens
-
case class
SExpPair(car: SExp, cdr: SExp, pos: Position) extends SExp with Product with Serializable
An s-expression is made of pairs, e.g., (foo bar) is represented as the pair with identifier foo as car and another pair -- with identifier bar as car and value nil as cdr -- as cdr.
An s-expression is made of pairs, e.g., (foo bar) is represented as the pair with identifier foo as car and another pair -- with identifier bar as car and value nil as cdr -- as cdr. Pairs are pretty-printed when converted to string. i.e., (foo bar) is stringified as (foo bar) and not (foo . (bar . ()))
-
case class
SExpQuoted(content: SExp, pos: Position) extends SExp with Product with Serializable
A quoted element, such as 'foo, '(foo (bar)), etc.
- trait SExpTokens extends Tokens
-
case class
SExpValue(value: Value, pos: Position) extends SExp with Product with Serializable
A literal value, such as 1, "foo", 'foo, etc.
-
case class
SchemeAcquire(exp: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Acquire a lock
-
case class
SchemeActor(name: String, xs: List[Identifier], defs: Map[String, (List[Identifier], List[SchemeExp])], pos: Position) extends SchemeExp with Product with Serializable
Define a behavior
-
case class
SchemeAnd(exps: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
An and expression: (and exps...)
-
case class
SchemeBecome(actor: SchemeExp, args: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Change the behavior of the current actor
-
case class
SchemeBegin(exps: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
A begin clause: (begin body...)
-
case class
SchemeCas(variable: Identifier, eold: SchemeExp, enew: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Compare-and-swap, concurrency synchronization primitive.
-
case class
SchemeCasVector(variable: Identifier, index: SchemeExp, eold: SchemeExp, enew: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Compare-and-swap on a vector
-
case class
SchemeCase(key: SchemeExp, clauses: List[(List[SchemeValue], List[SchemeExp])], default: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
A case expression: (case key ((vals1...) body1...) ...
A case expression: (case key ((vals1...) body1...) ... (else default...))
-
case class
SchemeCond(clauses: List[(SchemeExp, List[SchemeExp])], pos: Position) extends SchemeExp with Product with Serializable
A cond expression: (cond (test1 body1...) ...)
-
case class
SchemeCreate(actor: SchemeExp, args: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Create an actor from a behavior
-
case class
SchemeDefineFunction(name: Identifier, args: List[Identifier], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
A function definition: (define (name args...) body...)
-
case class
SchemeDefineVariable(name: Identifier, value: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
A variable definition: (define name value)
-
case class
SchemeDo(vars: List[(Identifier, SchemeExp, Option[SchemeExp])], test: SchemeExp, finals: List[SchemeExp], commands: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Do notation: (do ((<variable1> <init1> <step1>) ...) (<test> <expression> ...) <command> ...)
-
trait
SchemeExp extends AnyRef
Abstract syntax of Scheme programs (probably far from complete)
-
case class
SchemeFuncall(f: SchemeExp, args: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
A function call: (f args...)
-
case class
SchemeIf(cond: SchemeExp, cons: SchemeExp, alt: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
An if statement: (if cond cons alt) If without alt clauses need to be encoded with an empty begin as alt clause
-
case class
SchemeJoin(exp: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Wait for a thread (whose identifier is the value of exp) to terminate
-
case class
SchemeLambda(args: List[Identifier], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
A lambda expression: (lambda (args...) body...) Not supported: "rest"-arguments, of the form (lambda arg body), or (lambda (arg1 .
A lambda expression: (lambda (args...) body...) Not supported: "rest"-arguments, of the form (lambda arg body), or (lambda (arg1 . args) body...)
- trait SchemeLattice extends AnyRef
-
case class
SchemeLet(bindings: List[(Identifier, SchemeExp)], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Let-bindings: (let ((v1 e1) ...) body...)
-
case class
SchemeLetStar(bindings: List[(Identifier, SchemeExp)], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Let*-bindings: (let* ((v1 e1) ...) body...)
-
case class
SchemeLetrec(bindings: List[(Identifier, SchemeExp)], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Letrec-bindings: (letrec ((v1 e1) ...) body...)
-
case class
SchemeNamedLet(name: Identifier, bindings: List[(Identifier, SchemeExp)], body: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Named-let: (let name ((v1 e1) ...) body...)
-
case class
SchemeOr(exps: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
An or expression: (or exps...)
-
class
SchemePrimitives[Addr, Abs] extends Primitives[Addr, Abs]
This is where we define Scheme primitives
-
case class
SchemeQuoted(quoted: SExp, pos: Position) extends SchemeExp with Product with Serializable
A quoted expression: '(foo (bar baz)) The quoted expression is *not* converted to a Scheme expression, and remains a simple s-expression, because that's exactly what it should be.
-
case class
SchemeRelease(exp: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Release a lock
-
class
SchemeSemantics[V, Addr, Time] extends BaseSchemeSemantics[V, Addr, Time]
Extend base Scheme semantics with:
Extend base Scheme semantics with:
- atomic evaluation: parts of some constructs can be evaluated atomically without needing to introduce more states in the state graph. For example, (+ 1 1) can directly be evaluated to 2 without modifying the store. Also, to evaluate (+ 1 (f)), we can directly push the continuation and jump to the evaluation of (f), instead of evaluating +, and 1 in separate states.
-
case class
SchemeSend(target: SchemeExp, message: Identifier, args: List[SchemeExp], pos: Position) extends SchemeExp with Product with Serializable
Send a message to an actor
-
case class
SchemeSet(variable: Identifier, value: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
A set! expression: (set! variable value)
-
case class
SchemeSpawn(exp: SchemeExp, pos: Position) extends SchemeExp with Product with Serializable
Spawn a new thread to compute an expression
-
case class
SchemeTerminate(pos: Position) extends SchemeExp with Product with Serializable
Terminate the execution of an actor
-
case class
SchemeValue(value: Value, pos: Position) extends SchemeExp with Product with Serializable
A literal value (number, symbol, string, ...)
-
case class
SchemeVar(id: Identifier) extends SchemeExp with Product with Serializable
An identifier: name
- trait SemanticError extends AnyRef
-
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:
- 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.
- class SemanticsWithAnalysis[L, Exp, Abs, Addr, Time] extends Semantics[Exp, Abs, Addr, Time]
-
case class
SomePosition(p: scala.util.parsing.input.Position) extends Position with Product with Serializable
The actual wrapper
- abstract class Store[Addr, Abs] extends AnyRef
-
trait
StringLattice[S] extends LatticeElement[S]
A lattice for strings
-
trait
SymbolLattice[Sym] extends LatticeElement[Sym]
A lattice for symbols
- class TSchemePrimitives[Addr, Abs] extends SchemePrimitives[Addr, Abs]
- case class TaintAnalysis[Abs, Addr, Time]()(implicit evidence$26: JoinLattice[Abs], evidence$27: Address[Addr], evidence$28: Timestamp[Time]) extends Analysis[Set[(Position, Position)], SchemeExp, Abs, Addr, Time] with Product with Serializable
- case class TaintError(sources: Set[Position], sink: Position) extends SemanticError with Product with Serializable
- class TaintLattice[Abs] extends SchemeLattice
- sealed trait TaintStatus extends AnyRef
- case class Tainted(sources: Set[Position]) extends TaintStatus with Product with Serializable
- trait ThreadIdentifier[TID] extends AnyRef
- class Timeout extends AnyRef
- trait Timestamp[T] extends AnyRef
- trait TimestampWrapper extends AnyRef
- case class TimestampedKontStore[KontAddr](content: Map[KontAddr, Set[Kont[KontAddr]]], timestamp: Int)(implicit evidence$4: KontAddress[KontAddr]) extends KontStore[KontAddr] with Product with Serializable
- case class TypeError(name: String, operand: String, expected: String, got: String) extends SemanticError with Product with Serializable
- case class UnboundAddress(addr: String) extends SemanticError with Product with Serializable
- case class UnboundVariable(name: Identifier) extends SemanticError with Product with Serializable
-
case class
UnboundVariablesAnalysis[Abs, Addr, Time]()(implicit evidence$15: JoinLattice[Abs], evidence$16: Address[Addr], evidence$17: Timestamp[Time]) extends Analysis[Set[LamExp], LamExp, Abs, Addr, Time] with Product with Serializable
This is our unbound variables analysis.
This is our unbound variables analysis. We want to detect, for a lambda-calculus program, which evaluated variables may be unbound. We represent this by a set of lambda expressions, which is the lattice computed by this analysis: Set[LamExp]. This class defines how to update the current state of the analysis.
- case class UserError(reason: String, pos: Position) extends SemanticError with Product with Serializable
-
sealed abstract
class
Value extends AnyRef
S-expressions and related values
- case class ValueBoolean(value: Boolean) extends Value with Product with Serializable
- case class ValueCharacter(value: Char) extends Value with Product with Serializable
- case class ValueInteger(value: Int) extends Value with Product with Serializable
- case class ValueReal(value: Double) extends Value with Product with Serializable
- case class ValueString(value: String) extends Value with Product with Serializable
- case class ValueSymbol(sym: String) extends Value with Product with Serializable
-
case class
Var(x: Identifier, pos: Position) extends LamExp with Product with Serializable
A variable reference: x
- case class VariadicArityError(name: String, min: Int, got: Int) extends SemanticError with Product with Serializable
- trait VisitedSet[L[_]] extends AnyRef
- trait WithKey[A] extends AnyRef
- trait WorkList[L[_]] extends AnyRef
Value Members
- object AACKAlloc extends KAllocStrategy with Product with Serializable
- object AAMAACP4FBenchmarks extends Benchmarks
- object AAMKAlloc extends KAllocStrategy with Product with Serializable
- object ANF
- object ANFCompiler
- object ANFExp
- object ActorTimestamp
- object Address
- object AllInterleavings extends ExplorationType with Product with Serializable
- object BenchmarkGenerator
- object BenchmarkGeneratorConfig
- object BoolLattice
- object BottomTaint extends TaintStatus with Product with Serializable
- object Cardinality
- object CardinalityInf extends Cardinality with Product with Serializable
- object CardinalityPrimitiveLikeInf
- object CardinalityPrimitiveLikeNumber
- object CharLattice
- object ClassicalAddress extends AddressWrapper
- object Colors
-
object
Concrete
Some implementations of these abstract domains
- object ConcreteBooleanEfficient
- object ConcreteTimestamp extends TimestampWrapper
-
object
Config
This is where we parse the arguments given to the implementation
- object ConstantPropagation
- object ContextSensitiveTID
- object Count
- object CountInfinity extends Count with Product with Serializable
- object CountOne extends Count with Product with Serializable
- object CountingMap extends Serializable
- object DPOR extends ExplorationType with Product with Serializable
- object Dot
- object Effect
- object EffectKind
- object Environment
- object ExplorationTypeParser extends RegexParsers
- object Expression
- object Graph
- object GraphAnnotation
- object GraphDOTOutput extends GraphOutput
- object GraphJSONOutput extends GraphOutput
- object GraphNode
- object IdGen
- object InsensitiveTID
- object IntLattice
- object IsASchemeLattice extends Serializable
- object IsCSchemeLattice extends Serializable
- object IsSchemeLattice extends Serializable
- object IsTaintLattice extends Serializable
- object JSON
- object JoinLattice extends Serializable
- object Joined extends ExplorationType with Product with Serializable
- object KeyMap
- object KontStore
-
object
LamAnalysis
We want to perform a simple static analysis on lambda-calculus programs.
We want to perform a simple static analysis on lambda-calculus programs. We compute the possible unbound variables that are evaluated in the execution of a program.
-
object
LamExp
We have to tell scala-am that LamExp are actually expressions
- object LamLattice extends Serializable
-
object
LamLatticeImpl
Here's an implementation of this lattice
- object LatticeElement
-
object
Main
Fork of Scala-AM (written by Quentin Stiévenart) https://github.com/acieroid/scala-am with the final goal to parallelize it: https://bitbucket.org/OPiMedia/scala-par-am
Fork of Scala-AM (written by Quentin Stiévenart) https://github.com/acieroid/scala-am with the final goal to parallelize it: https://bitbucket.org/OPiMedia/scala-par-am
Before looking at this, we recommend seeing how to use this framework. A detailed example is available in examples/LambdaCalculus.scala.
This is the entry point. It parses the arguments, parses the input file and launches an abstract machine on the parsed expression (or launches a REPL if no input file is given). The pipeline goes as follows:
- The input program is parsed. For Scheme programs, it is done by:
- Parsing the file as a list of s-expressions (exp/SExp.scala, exp/SExpParser.scala)
- Compiling these s-expressions into Scheme expressions (exp/scheme/Scheme.scala)
2. To run the program, we need an abstract machine and some semantics. Semantics definitions have to implement the Semantics interface (semantics/Semantics.scala).
3. Once the abstract machine is created and we have a semantics for the program we want to analyze, the abstract machine can perform its evaluation, relying on methods of the semantics class to know how to evaluate expressions. The abstract machine only deals with which states to evaluate in which order, where to store values, where to store continuations, how to push and pop continuations, etc. The semantics encode what to do when encountering a program construct. For example, the semantics can tell what to evaluate next, that a continuation needs to be pushed, or that a variable needs to be updated. The abstract machine will then respectively evaluate the expression needed, push the continuation, or update the variable.
Multiple abstract machine implementations are available, defined in the machine/ directory. Every abstract machine implementation has to implement the AbstractMachine interface (machine/AbstractMachine.scala).
The abstract machine also uses a lattice to represent values. Lattices should implement the JoinLattice trait that can be found in lattice/JoinLattice.scala, which provides the basic features of a lattice.
If you want to:
- Support a new language: you will need:
- A parser, you can look into exp/SExpParser.scala as an inspiration. If your language is s-expression based, you can use this parser and compile s-expressions into your abstract grammar. To do so, look at exp/scheme/Scheme.scala.
- An abstract grammar, look at exp/SExp.scala or the SchemeExp class in exp/scheme/Scheme.scala.
- A semantics, look at semantics/anf/ANFSemantics.scala for a simple example.
- Support for your language operations at the lattice level. For this, you'll probably need to extend the lattices (see lattice/scheme/SchemeLattice.scala, lattice/scheme/ModularLattice.scala)
- Play with abstract machines, you can look into AAM.scala.
- Implement some kind of analysis, look at examples/LambdaCalculus.scala and examples/TaintAnalysis.scala.
- The input program is parsed. For Scheme programs, it is done by:
-
object
MainAsScalaParAM
Execute some abstract machines on some Scheme programs depending of some parameters.
Execute some abstract machines on some Scheme programs depending of some parameters.
Run with --help command line parameter to show all options: $ java -cp scala-am.jar MainAsScalaParAM --help
This main program is used to interact with Scala-Par-AM https://bitbucket.org/OPiMedia/scala-par-am/ a parallel version of this Scala-AM.
- object MayFail
- object MboxSizeUnbounded extends MboxSize with Product with Serializable
- object MonoBenchmarks extends Benchmarks
- object OneInterleaving extends ExplorationType with Product with Serializable
- object P4FKAlloc extends KAllocStrategy with Product with Serializable
- object Position
- object Profiler
- object RandomInterleaving extends ExplorationType with Product with Serializable
- object ReadEffect extends EffectKind with Product with Serializable
- object RealLattice
- object SExpList
- object SExpParser extends TokenParsers
- object ScalaAM
- object Scheme
-
object
SchemeCompiler
Object that provides a method to compile an s-expression into a Scheme expression
- object SchemeExp
- object SchemeLattices
- object SchemeOps
-
object
SchemeRenamer
Object that provides a method to rename variables in a Scheme program in order to have only unique names.
Object that provides a method to rename variables in a Scheme program in order to have only unique names. For example, (let ((x 1)) (let ((x 2)) x)) will be converted to (let ((_x0 1)) (let ((_x1 2)) _x1)). This is useful to perform ANF conversion.
-
object
SchemeUndefiner
Remove defines from a Scheme expression, replacing them by let bindings.
Remove defines from a Scheme expression, replacing them by let bindings. For example: (define foo 1) (define (f x) x) (f foo) Will be converted to: (letrec ((foo 1) (f (lambda (x) x))) (f foo)) Which is semantically equivalent with respect to the end result
- object SimpleBenchmarks extends Benchmarks
- object Store
- object StringLattice
- object SymbolLattice
- object TaintAnalysis extends Serializable
- object ThreadIdentifier
- object Timeout
- object Timestamp
- object Type
- object Untainted extends TaintStatus with Product with Serializable
- object Util
- object ValueNil extends Value
- object ValueSensitiveAddress extends AddressWrapper
- object VisitedSet
- object WithKey
- object WorkList
- object WriteEffect extends EffectKind with Product with Serializable
- object ZeroCFA extends TimestampWrapper
Implementation of a CESK machine following the AAM approach (Van Horn, David, and Matthew Might. "Abstracting abstract machines." ACM Sigplan Notices. Vol. 45. No. 9. ACM, 2010).
A difference with the paper is that we separate the continuation store (KontStore) from the value store (Store). That simplifies the implementation of both stores, and the only change it induces is that we are not able to support first-class continuation as easily (we don't support them at all, but they could be added).
Also, in the paper, a CESK state is made of 4 components: Control, Environment, Store, and Kontinuation. Here, we include the environment in the control component, and we distinguish "eval" states from "continuation" states. An eval state has an attached environment, as an expression needs to be evaluated within this environment, whereas a continuation state only contains the value reached.