Module Pulselib.PulseDomainInterface

High-level Pulse Operations

If you do any mutations of the state in pulse that go beyond what PulseOperations offers you may want these modules (but consider adding what you need to PulseOperations or to one of the models modules if appropriate). In addition to defining short names for safe versions of stack/heap/... it ensures only those safe versions are used. Do not use lower-level modules directly!

High-level modules operating on the entire biabductive state

module AbductiveDomain = PulseAbductiveDomain
module Stack = AbductiveDomain.Stack
module Memory = AbductiveDomain.Memory
module AddressAttributes = AbductiveDomain.AddressAttributes
module CanonValue = AbductiveDomain.CanonValue

Low-level modules operating on individual elements of the abductive domain

module BaseStack = CanonValue.Stack
module BaseMemory = CanonValue.Memory
module CanonAccess = BaseMemory.Access
module CanonAccessSet = BaseMemory.Access.Set
module BaseAddressAttributes = CanonValue.Attributes
module Decompiler = PulseAbductiveDecompiler
module NonDisjDomain = PulseNonDisjunctiveDomain
module PathContext = PulsePathContext

Miscellaneous

module AccessResult = PulseAccessResult
module DecompilerExpr = PulseDecompilerExpr
module Diagnostic = PulseDiagnostic
module ExecutionDomain = PulseExecutionDomain
module LatentIssue = PulseLatentIssue

Unsafe modules, use with caution

Misusing these modules may miss abducing addresses to the pre-condition or mistakenly manipulate non-normalized values. See PulseAbductiveDomain for more information.

These can safely be used when reading summaries, where all values have already been normalized on creation.

module BaseDomain = PulseBaseDomain
module UnsafeStack = PulseBaseStack
module UnsafeMemory = PulseBaseMemory
module UnsafeAttributes = PulseBaseAddressAttributes

Enforce short form usage

include sig ... end
module PulseAbductiveDomain = PulseAbductiveDomain
module PulseAccessResult = PulseAccessResult
module PulseBaseDomain = PulseBaseDomain
module PulseBaseStack = PulseBaseStack
module PulseBaseMemory = PulseBaseMemory
module PulseBaseAddressAttributes = PulseBaseAddressAttributes
module PulseAbductiveDecompiler = PulseAbductiveDecompiler
module PulseDiagnostic = PulseDiagnostic
module PulseExecutionDomain = PulseExecutionDomain
module PulseLatentIssue = PulseLatentIssue
module PulsePathContext = PulsePathContext
include module type of struct include PulseResult.Type end

for opening locally

type ('ok, 'err) pulse_result = ('ok, 'err) PulseResult.t =
  1. | Ok of 'ok
  2. | Recoverable of 'ok * 'err list
  3. | FatalError of 'err * 'err list