asil-1.2: src/LanguageAst.ag
-- This file encodes the abstract syntax of the core instrumentation language.
-- With this language, we can specify the instrumentation of object-oriented
-- programming languages.
-- We provide a high-level Haskell embedding for this language, which provides
-- abstraction facilities and type checking (See @Instr.hs@).
-- The root of the specification, encapsulating an |Instr|.
DATA Spec
| Instr expr : Instr
-- An |Instr| is a specification of how to (conditionally) intrument an instrumentable
-- program point. A program point is instrumentable when it is member of the library to
-- be transformed. Program points in native code, or code from non-transformed libraries,
-- are thus not instrumentable.
--
-- There are two main instrumentations: to match against program points such as function
-- calls (binding names to runtime values), and to specify function calls (parametrized
-- by bound runtime values) to add to the program point (binding names to return values).
--
-- Both operations have a runtime notion of success: a match succeeds if the associated
-- pattern matches the program point. A method call succeeds, unless its implementation
-- calls an special abort routine. The success of a match can be determined statically:
-- matches are resolved statically, binding symbolic names to the runtime values that
-- play a role upon execution of the program point.
--
-- Function calls can only be resolved at runtime. For function calls that may be resolved
-- at compile time, we define special instrumentation primitives (such as |Equal| and
-- |TypeOf|). This mechanism allows us to impose constraints on symbolic names.
--
-- The instrumentations can be composed sequentially or in parallel. Sequential composition
-- |p `Seq` q|, performs |q| if |p| succeeds. Parallel composition |p `Alt` q|, performs
-- both |p| and |q| (in the order of appearance).
DATA Instr
-- Combinators for combining instrumentations
| Nop -- always succeeding instrumentation (unit to |Seq|)
| Fail msg : {Maybe String} -- always failing instrumentaiton (unit to |Alt|)
| Seq left : Instr -- sequential composition. Alternatives may occur
right : Instr -- as LHS.
| Alt left : Instr -- parallel composition. If |tryBoth| is |True|, then
right : Instr -- the right alternative is always tried. Otherwise,
tryBoth : Bool -- only when the first alternative fails.
| Loop instr : Instr -- repeatedly apply instrumentation until it fails (requires side effect)
-- Primitive combinators
| CallFun name : Val -- invoke runtime function
inps : Params -- with given input assignments
outs : Params -- and output assignments
| CallProp
prop : Val -- invoke runtime property
inps : Params -- with given input assignments
outs : Params -- and output assignments
| Match spec : Match -- match against program point
| Type val : Val -- statically declares type of a value
tp : Val -- value of type 'Type'
-- Combinators to force/check static or dynamic behavior
| Static instr : Instr -- enforce static treatment; error if this cannot be realized
| Dyn instr : Instr -- ... unless explicitly marked as dynamic
-- Static functions that may either be static or dynamic
| Assign var : Int -- assigns a value to a variable
val : Val -- side-effectful operation
| Assert guard : Val -- tests against a boolean condition
| BinOp left : Val -- binary operator
right : Val
out : Val
op : BinOp
| UnOp inp : Val -- unary operator
out : Val
op : UnOp
| Scan format : Val -- describes a regular expression
str : Val -- matches a string against a regular expression
outs : Params -- succesful match binds values to symbols in grammars.
| Pretty format : Val -- pretty prints |inps| according to some format
inps : Params -- description in |format|, and stores it as string value
out : Val -- in |out|
| TypeOf inp : Val -- obtain static or runtime type of a value, with a preference
out : Val -- for static if possible (use static/dynamic combinators to enforce)
| Coerce coe : Coercion -- apply a coercion
inp : Val
out : Val
-- Control-flow graph operations
| Last instr : Instr -- execute instrs on matching preceding join points. Returns the outcome of the last one; fails otherwise.
-- |Match| is a specification of a match against a join point.
-- When more static information about a join point is available,
-- we can make more interesting matches.
DATA Match
| EnterBlock id : Val -- entry-point of a block of statements
cyc : Val -- ... on a cyclic control-flow path
excp : Val -- maybe-value (if defined, then points to caught exception)
| LeaveBlock id : Val -- exit-point of a block of statements
cyc : Val -- ... on a cyclic control-flow path
| FailBlock id : Val -- failure to execute a block of statements
excp : Val -- exception that occurred in the block of statements
-- Matches
| EnterFun id : Val -- entry of a function
name : Val -- name of the function
kind : Val -- kind of function: method, property, function
inps : Params -- parameters of the function
| LeaveFun id : Val -- succesful exit of a function
name : Val -- name of the function
kind : Val -- kind of the function: method, property, function
outs : Params -- return value(s) of the function
| FailFun id : Val -- exit a function with failure
name : Val -- name of the function
kind : Val -- kind of the function: method, property, function
excp : Val -- exception that occurred in the function
-- Matches on function calls
| BeginCall id : Val -- begin of function call
name : Val
kind : Val -- essential difference with EnterFun: instruments the
inps : Params -- caller instead of the callee
| DoneCall id : Val -- end of method call.
name : Val
kind : Val
outs : Params
| FailedCall id : Val -- a failed method call (that exited with an exception)
name : Val
kind : Val
excp : Val -- the exception thrown
-- Matches on Coercions
| BeginCoerce id : Val -- start of a coercion
inp : Val -- value before coercion
coe : Coercion -- the coercion
| DoneCoerce id : Val -- succesful coercion
outp : Val -- value after coercion
coe : Coercion -- the coercion
| FailedCoerce id : Val -- failed coercion
excp : Val -- exception
inp : Val -- value that could not be coerced
coe : Coercion -- the coercion
-- Parameters and values
DATA Params
| Any val : Val
| Nil
| Cons hd : Param
tl : Params
DATA Param
| Param val : Val
TYPE Vals = [Val]
TYPE MaybeVal = MAYBE Val
-- | A value is either a constant, a field of a class, or a symbolic value.
-- Each symbolic value is associated with an integer value. Some symbolic values
-- may have a statically known value; others are available at runtime.
-- Constants are statically known values. This is never the case for objects and
-- and fields.
DATA Val
| Int val : Int
| UInt val : Word32
| Bool val : Bool
| String val : String
| Array elems : Vals
| Sym sym : Int
| Ind arr : Val
ind : Val
| Prop obj : Val
key : String
| Dyn obj : Val
key : Val
| Type val : Type
| Method name : String
-- Types (act as first-class constant values)
DATA Type
| Any
| Bool
| Int
| UInt
| Double
| String
| Array elem : Type
| Base -- the base type of all object types
| Object name : String
| Method -- a method (lost type info)
-- Coercions
DATA Coercion
| None
| Any
| Any'
| String
| Double
| Int
| UInt
| Instance
-- Unary operators
DATA UnOp
| Abs -- absolute value
| Not -- logical negation
| Neg -- numerical negation
-- Manipulate 'Maybe' values
| IsJust -- tests if it is a 'just' value (returns |True| if yes)
| IsNothing -- tests if its a nothing value (returns |True| if yes)
| ExtractJust -- takes the value out of a 'just' value
-- Manipulate 'Array' values
| Length -- get the length of an array
-- Binary operators
DATA BinOp
-- logical operators
| And
| Or
-- relation to operator
| Rel rel : Rel
-- arithmetic operators
| Add
| Sub
| Mul
| Div
| Mod
| Max
| Min
-- Binary relations
DATA Rel
| Equal
| Smaller
| Greater
| SmallerEqual
| GreaterEqual
| Negate rel : Rel