Semantics (bap-primus.Bap_primus.Std.Primus.Lisp.Semantics)

type value = unit Bap_core_theory.Theory.Value.t

the representation of semantic values.

since 2.4.0

type Bap_core_theory.KB.conflict +=

| Unresolved_definition of string

occurs when no matching definition is found

The reason why no match is selected is provided as the payload.

type Bap_core_theory.KB.conflict +=

| Illtyped_program of Type.error list

occurs when the Lisp program is ill-typed

type Bap_core_theory.KB.conflict +=

| Failed_primitive of Bap_core_theory.KB.Name.t * string

occurs when a primitive fails.

See also, failp

since 2.4.0

val program : 
  (Bap_core_theory.Theory.Source.cls, program) Bap_core_theory.KB.slot

a property of the program source object in which a Lisp program is stored.

This property is used by the Lisp semantics provider to lookup for the definitions.

val context : 
  (Bap_core_theory.Theory.Unit.cls, context) Bap_core_theory.KB.slot

Primus Lisp definitions constraints.

The set of type classes that describe the unit constraints and limits applicability of Primus Lisp definitions to the selected compilation unit.

Each Primus Lisp definition has a context class of its applicability. The definition will only be used if its context is a subtype of the unit context.

since 2.5.0

val definition : 
  (Bap_core_theory.Theory.program, Bap_core_theory.Theory.Label.t option)
    Bap_core_theory.KB.slot

The Primus Lisp definition to which the program belongs.

This property stores the label to the original program for which the semantics was requested. It is useful in the implementation of primitives that require access to the context, for example, to access the original instruction address (when Primus Lisp is used to represent the semantics of an instruction) or to the declared attribute of the Primus Lisp definition.

val name : 
  (Bap_core_theory.Theory.program, Bap_core_theory.KB.Name.t option)
    Bap_core_theory.KB.slot

the name of a lisp program

val args : 
  (Bap_core_theory.Theory.program,
    unit Bap_core_theory.Theory.Value.t list option)
    Bap_core_theory.KB.slot

the arguments of a lisp program

val symbol : 
  (Bap_core_theory.Theory.Value.cls, Core_kernel.String.t option)
    Bap_core_theory.KB.slot

a statically known symbolic value

val static : 
  (Bap_core_theory.Theory.Value.cls, Bitvec.t option) Bap_core_theory.KB.slot

a statically known value of an operation

val enable : ?stdout:Stdlib.Format.formatter -> unit -> unit

enable () enables the semantics of Primus Lisp programs.

This function registers a rule in the knowledge base that has the following form,

              -- reifies Primus Lisp definitions
              primus-lisp-semantics ::=
                bap:primus-lisp-program
                core-theory:unit-target
                core-theory:unit-source
                core-theory:label-unit
                bap:lisp-args
                bap:lisp-name
                -----------------------
                core-theory:semantics

The rule provides semantics to the program objects that have a unit with Primus Lisp source code available (the program property).

This function is by default called by the primus-lisp plugin. This plugin also implements core primitives and provides a loader that will load all features specified via the --primus-lisp-load command-line argument to any Primus Lisp unit. Therefore, if the primus-lisp plugin is loaded in order to reify a lisp definition into a Theory.Semantics value, use the following code,

let reify_def name : unit Theory.eff =
  Theory.Label.for_name name >>= fun obj ->
  Unit.create Theory.Target.unknown >>= fun unit ->
  KB.provide Theory.Label.unit obj (Some unit) >>= fun () ->
  KB.collect Theory.Semantics.slot obj

Note, if you don't want to use the program loader provided by the primus-lisp plugin then just set manually the source field with the Lisp program of you choice.

parameter stdout
is the formatter that is used by the msg form to print messages.

val declare : 
  ?types:Type.signature ->
  ?docs:string ->
  ?package:string ->
  ?body:
    (Bap_core_theory.Theory.Target.t ->
      (Bap_core_theory.Theory.Label.t ->
        value list ->
        unit Bap_core_theory.Theory.eff)
        Bap_core_theory.KB.t) ->
  string ->
  unit

Primus primitives.

New primitives are implemented as a knowledge base promises to provide Theory.Semantics.slot for an object that has the primitive property.

Example,

KB.promise Theory.Semantics.slot @@ fun obj ->
KB.collect Sema.primitive obj >>= function
| None -> Insn.empty
| Some p -> match Primitive.name p with
  | "boo" ->
    Theory.instance () >>= Theory.require >>=
    fun (module CT) ->
    (* ... operations in CT ... *)

  | _ -> !!Insn.empty

val signal : 
  ?params:[< Type.parameters ] ->
  ?docs:string ->
  (Bap_core_theory.Theory.program, 'p) Bap_core_theory.KB.slot ->
  (Bap_core_theory.Theory.Label.t -> 'p -> value list Bap_core_theory.KB.t) ->
  unit

signal ~params ~docs property args declares a signal.

Emits a signal with arguments args l v, when the property value of a program label l changes to v. The name of the signal is the same as the name of the property.

The signal triggers all methods with the same method name as the signal.

since 2.4.0

val failp : 
  ('a, Stdlib.Format.formatter, unit, 'b Bap_core_theory.KB.t)
    Core_kernel.format4 ->
  'a

failp err_msg args... terminates a primitive with error.

Must be called from a primitive implementation to stop the evaluation with the Failed_primitive conflict.

This conflict should used to report programmer errors that are not representable via the type system (or slipped through the gradual type checker).

since 2.4.0

val documentation : 
  Bap_core_theory.Theory.Unit.t ->
  Doc.index Bap_core_theory.KB.t

documentation unit documentation for unit's lisp source.

Typechecks and loads the unit lisp source and generates its documentation.

module Value : sig ... end

Pure semantic value.

module Effect : sig ... end

Effectful semantic values.