bap-std 2.3.0 · OCaml Package

IR language term.

Term is a building block of the Intermediate Representation of the binary program.

This module provides functions that are overloaded for different term classes. Term class is denoted with an explicit instance of type ('a,'b)cls, where 'a stands for the parent term and 'b for the child term.

Example

Give a block

# let b = Blk.create ();;

val b : Blk.t =
          00000003:

We can append a definition to it with an overloaded Term.append

# let b = Term.append def_t b d_1;;

val b : blk term =
          00000003:
          00000001: x := y + z

Update a value of a definition in the block:

# let b = Term.update def_t b d_2;;

val b : blk term =
          00000003:
          00000001: x := true

type 'a t = 'a term

term type

val clone : 'a t -> 'a t

clone term creates an object with a fresh new identifier that has the same contents as term, i.e., that is syntactically the same. The clone operation is shallow, all subterms of term are unchanged.

val same : 'a t -> 'a t -> bool

same x y returns true if x and y represents the same entity, i.e., Tid.(tid x = tid y)

val name : 'a t -> string

name t returns a string representation of a term t identity

val tid : 'a t -> tid

tid entity returns a unique identifier of the entity

val length : ('a, 'b) cls -> 'a t -> int

length t p returns an amount of terms of t class in a parent term p

val find : ('a, 'b) cls -> 'a t -> tid -> 'b t option

find t p id is Some c if term p has a subterm of type t such that tid c = id.

val find_exn : ('a, 'b) cls -> 'a t -> tid -> 'b t

find_exn t p id like find but raises Not_found if nothing is found.

val update : ('a, 'b) cls -> 'a t -> 'b t -> 'a t

update t p c if term p contains a term with id equal to tid c then return p with this term substituted with p

val remove : ('a, _) cls -> 'a t -> tid -> 'a t

remove t p id returns a term that doesn't contain element with the a given id

val change : 
  ('a, 'b) cls ->
  'a t ->
  tid ->
  ('b t option -> 'b t option) ->
  'a t

change t p id f if p contains subterm with of a given kind t and identifier id, then apply f to this subterm. Otherwise, apply f to None. If f return None, then remove this subterm (a given it did exist), otherwise, update parent with a new subterm.

val enum : ?rev:bool -> ('a, 'b) cls -> 'a t -> 'b t seq

enum ?rev t p enumerate all subterms of type t of the a given term p

val to_sequence : ?rev:bool -> ('a, 'b) cls -> 'a t -> 'b t seq

to_sequence ?rev t p is a synonym for enum.

val map : ('a, 'b) cls -> 'a t -> f:('b t -> 'b t) -> 'a t

map t p ~f returns term p with all subterms of type t mapped with function f

val filter_map : ('a, 'b) cls -> 'a t -> f:('b t -> 'b t option) -> 'a t

filter_map t p ~f returns term p with all subterms of type t filter_mapped with function f, i.e., all terms for which function f returned Some thing are substituted by the thing, otherwise they're removed from the parent term

val concat_map : ('a, 'b) cls -> 'a t -> f:('b t -> 'b t list) -> 'a t

concat_map t p ~f substitute subterm c of type t in parent term p with f c. If f c is an empty list, then c doesn't occur in a new parent term, if f c is a singleton list, then c is substituted with the f c, like in map. If f c is a list of n elements, then in the place of c this n elements are inserted.

val filter : ('a, 'b) cls -> 'a t -> f:('b t -> bool) -> 'a t

filter t p ~f returns a term p with subterms c for which f c = false removed.

val first : ('a, 'b) cls -> 'a t -> 'b t option

first t p returns the first subterm of type t of a given parent p

val last : ('a, 'b) cls -> 'a t -> 'b t option

last t p returns a last subterm of type t of a given parent p

val next : ('a, 'b) cls -> 'a t -> tid -> 'b t option

next t p id returns a term that is after a term with a given id, if such exists.

val prev : ('a, 'b) cls -> 'a t -> tid -> 'b t option

prev t p id returns a term that precedes a term with a given id, if such exists.

val after : ('a, 'b) cls -> ?rev:bool -> 'a t -> tid -> 'b t seq

after t ?rev p tid returns all subterms in term p that occur after a term with a given tid. if rev is true or omitted then terms are returned in the evaluation order. Otherwise they're reversed. If there is no term with a given tid, then an empty sequence is returned.

val before : ('a, 'b) cls -> ?rev:bool -> 'a t -> tid -> 'b t seq

before t ?rev p tid returns all term that occurs before definition with a given tid in blk. If there is no such definition, then the sequence will be empty.

parameter rev
has the same meaning as in after.

val append : ('a, 'b) cls -> ?after:tid -> 'a t -> 'b t -> 'a t

append t ~after:this p c returns the p term with c appended after this term. If after is not specified, then append def to the end of the parent term (if it makes sense, otherwise it is just added). If this doesn't occur in the p term then do nothing. The term tid is preserved.

val prepend : ('a, 'b) cls -> ?before:tid -> 'a t -> 'b t -> 'a t

prepend t ~before:this p c returns the p with c inserted before this term. If before is left unspecified, then insert the c at the beginning of the p if it is a sequence, otherwise just insert. If this is specified but doesn't occur in the p then p is returned as is. In all cases, the returned term has the same tid as p.

val nth : ('a, 'b) cls -> 'a t -> int -> 'b t option

nth t p n returns n'th t-term of parent p.

val nth_exn : ('a, 'b) cls -> 'a t -> int -> 'b t

nth_exn t p n same as nth, but raises exception if n is not a valid position number.

Attributes

Terms attribute set can be extended, using universal values. A value of type 'a tag is used to denote an attribute of type 'a with the name Value.Tag.name tag.

With the provided interface Term can be treated as an extensible record.

val set_attr : 'a t -> 'b tag -> 'b -> 'a t

set_attr term attr value attaches an value to attribute attr in term

val attrs : 'a t -> Dict.t

attrs term attrs returns the set of attributes associated with a term

val with_attrs : 'a t -> Dict.t -> 'a t

with_attrs term attributes returns a term with a new set of attributes

val get_attr : 'a t -> 'b tag -> 'b option

get_attr term attr returns a value of the a given attr in term

val has_attr : 'a t -> 'b tag -> bool

has_attr term attr is true if term has attribute attr

val del_attr : 'a t -> 'b tag -> 'a t

del_attr term attr deletes attribute attr from term

Predefined attributes

val origin : tid tag

a term was artificially produced from a term with a given tid.

val synthetic : unit tag

a term was introduced artificially by an analysis.

val live : unit tag

a term is identified as always non dead

val dead : unit tag

a term is identified as dead

val visited : unit tag

to mark a term as visited by some algorithm

val precondition : exp tag

precondition must on the entrance to the subroutine

val invariant : exp tag

invariant must be always true while the term is evaluated

val postcondition : exp tag

must hold just after the term is left

Higher order mapping

class mapper : object ... end

Mapper performs deep identity term mapping. If you override any method make sure that you didn't forget to invoke parent's method, as OCaml will not call it for you.

class 'a visitor : object ... end

Visitor performs deep visiting. As always, don't forget to overrid parent methods. The visitor comes with useful enter_T leave_T that are no-ops in this visitor, so if you inherit directly from it, then you may not call to the parent method.

val switch : 
  ('p, 't) cls ->
  program:(program term -> 'a) ->
  sub:(sub term -> 'a) ->
  arg:(arg term -> 'a) ->
  blk:(blk term -> 'a) ->
  phi:(phi term -> 'a) ->
  def:(def term -> 'a) ->
  jmp:(jmp term -> 'a) ->
  't term ->
  'a

switch cls t ~program ~sub .. ~jmp performs a pattern matching over a term t based on its type class cls. It is guaranteed that only one function will be called for a term.

val proj : 
  ('p, 't) cls ->
  ?program:(program term -> 'a option) ->
  ?sub:(sub term -> 'a option) ->
  ?arg:(arg term -> 'a option) ->
  ?blk:(blk term -> 'a option) ->
  ?phi:(phi term -> 'a option) ->
  ?def:(def term -> 'a option) ->
  ?jmp:(jmp term -> 'a option) ->
  't term ->
  'a option

proj cls t ?case a special case of pattern matching, where all cases by default returns None

val cata : 
  ('p, 't) cls ->
  init:'a ->
  ?program:(program term -> 'a) ->
  ?sub:(sub term -> 'a) ->
  ?arg:(arg term -> 'a) ->
  ?blk:(blk term -> 'a) ->
  ?phi:(phi term -> 'a) ->
  ?def:(def term -> 'a) ->
  ?jmp:(jmp term -> 'a) ->
  't term ->
  'a

cata cls ~init t ?case performs a pattern matching. All methods by default returns init. Note: cata stands for catamorphism

val slot : 
  (Bap_core_theory.Theory.Program.Semantics.cls, blk term list)
    Bap_knowledge.Knowledge.slot

the graphical representation of the program

package bap-std

Example

Attributes

Higher order mapping