package bap-std

  1. Overview
  2. Docs
package bap-std
Legend:
Library
Module
Module type
Parameter
Class
Class type

Effect analysis.

Effect analysis describes how an expression computation interacts with the outside world. By the outside world we understand the whole of the CPU state (including the hidden state) and the memory. We distinguish, so far, between the following sorts of effects:

  • coeffects - a value of an expression depends on the outside world, that is further subdivided by the read effect, when an expression reads a CPU register, and the load effect, when an expression an expression accesses the memory.
  • effects - a value modifies the state of the world, by either storing a value in the memory, or by raising a CPU exception via the division by zero or accessing the memory.

An expression that doesn't have effects or coeffects is idempotent and can be moved arbitrary in a tree, removed or substituted. An expression that has only coeffects is generative and can be reproduced without a significant change of semantics.

Examples:

  • x ^ x, x+1, x - have coeffects;
  • x[y] - has both effects (may raise pagefault) and coeffects;
  • 7 * 8, 42 - have no effects.
  • since 1.3
type t

a set of expression effects

val none : t

an expression doesn't have any effects

val read : t

an expression reads a register (nonvirtual) variable.

val load : t

an expression loads a value from a memory

val store : t

an expression stores a value in a memory

val raise : t

an expression raises a CPU exception

val reads : t -> bool

reads eff if read in eff

val loads : t -> bool

loads eff if load in eff

val stores : t -> bool

stores eff if load in eff

val raises : t -> bool

raises eff if raise in eff

val has_effects : t -> bool

has_effects eff if stores eff || raises eff

val has_coeffects : t -> bool

has_coeffects eff if loads eff || reads eff

compute x computes a set of effects produced by x. The result is a sound overapproximation of the real effects, i.e., if an effect is computed then it may really happen, but if it is not computed, then it is proved that it is not possible for the expression to have this effect.

The analysis applies a simple abstract interpretation to approximate arithmetic and prove an absence of the division by zero. The load/store/read analysis is more precise than the division by zero, as the only source of the imprecision is a presence of conditional expressions.

Requires: normalized and simplified expression.

Warning: the above should be either relaxed or expressed in the type system.

val compute : exp -> t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct