-- 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