Module Core.QuerySource

Generic query mechanism for extracting information from domains.

Sourcetype ('a, _) query = ..

Extensible type of queries

Sourceval join_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Join two queries

Sourceval meet_query : ?ctx:'a Context.ctx option -> ?lattice:'a Lattice.lattice option -> ('a, 'r) query -> 'r -> 'r -> 'r

Meet two queries

Registration

****************

Sourcetype query_pool = {
  1. pool_join : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered queries

Sourcetype query_info = {
  1. join : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. query_pool -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registraction info for new queries

Sourceval register_query : query_info -> unit

Register a new query

Sourcetype lattice_query_pool = {
  1. pool_join : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. pool_meet : 'a 'r. 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Pool of registered lattice queries. Lattice queries are queries that return elements of the global abstract state lattice. Join/meet operators are enriched with the lattice and the context so that we can compute join/meet over the abstract elements.

Sourcetype lattice_query_info = {
  1. join : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
  2. meet : 'a 'r. lattice_query_pool -> 'a Context.ctx -> 'a Lattice.lattice -> ('a, 'r) query -> 'r -> 'r -> 'r;
}

Registration info for new lattice queries

Sourceval register_lattice_query : lattice_query_info -> unit

Register a new lattice query

Common queries

******************

Sourcetype query +=
  1. | Q_defined_variables : string option -> ('a, Ast.Var.var list) query
    (*

    Extract the list of defined variables, in a given function call site, or in all scopes

    *)
  2. | Q_allocated_addresses : ('a, Ast.Addr.addr list) query
    (*

    Query to extract the list of addresses allocated in the heap

    *)
  3. | Q_variables_linked_to : Ast.Expr.expr -> ('a, Ast.Var.VarSet.t) query
    (*

    Query to extract the auxiliary variables related to an expression

    *)