Class: SeccompTools::Symbolic::State

Inherits:
Object
  • Object
show all
Defined in:
lib/seccomp-tools/symbolic/state.rb

Overview

A snapshot of the classic-BPF machine at one point along one path of the walk: the two registers (A and X), the 16 scratch-memory slots, and the path condition (the Constraints that must hold to have reached here). The walk fills values in as it interprets instructions, starting from State.initial.

A State is treated as immutable - stepping an instruction produces a new state via #with, so the many paths of the walk can safely share the parts they have in common.

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(a:, x:, mem:, path:) ⇒ State

Returns a new instance of State.

Parameters:



37
38
39
40
41
42
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 37

def initialize(a:, x:, mem:, path:)
  @a = a
  @x = x
  @mem = mem
  @path = path
end

Instance Attribute Details

#a ⇒ Expr (readonly)

Returns Register A (the accumulator).

Returns:

  • (Expr) —

    Register A (the accumulator).



16
17
18
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 16

def a
  @a
end

#mem ⇒ Array<Expr> (readonly)

Returns The 16 scratch-memory slots (+mem+).

Returns:

  • (Array<Expr>) —

    The 16 scratch-memory slots (+mem+).



20
21
22
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 20

def mem
  @mem
end

#path ⇒ Array<Constraint> (readonly)

Returns The path condition accumulated so far.

Returns:

  • (Array<Constraint>) —

    The path condition accumulated so far.



22
23
24
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 22

def path
  @path
end

#x ⇒ Expr (readonly)

Returns Register X (the index register).

Returns:

  • (Expr) —

    Register X (the index register).



18
19
20
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 18

def x
  @x
end

Class Method Details

.initial ⇒ State

The starting state, as the kernel sets it up: both registers zero (a classic BPF program is guaranteed A = X = 0 on entry - the cBPF-to-eBPF converter clears them first), the scratch slots unknown, and no facts assumed. The slots stay Expr.opaque because nothing can rely on them: the kernel rejects a filter that reads a slot before writing it.

Returns:



29
30
31
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 29

def self.initial
  new(a: Expr.imm(0), x: Expr.imm(0), mem: Array.new(16, Expr.opaque), path: [])
end

Instance Method Details

#==(other) ⇒ Boolean Also known as: eql?

Parameters:

Returns:

  • (Boolean) 


71
72
73
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 71

def ==(other)
  other.is_a?(State) && key == other.key
end

#hash ⇒ Integer

Returns:

  • (Integer) 


77
78
79
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 77

def hash
  key.hash
end

#key ⇒ String

A string that identifies this state exactly, joined from each part's Expr#key / Constraint#key (the same identity, one level up). The walk uses it to skip a (line, state) pair it has already visited, which keeps merging control-flow from blowing up. Both #== and #hash are decided on it; see Expr#key for why the key is a string. The ; / , separators appear in no part's key, so the join stays injective.

Returns:

  • (String) 


57
58
59
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 57

def key
  @key ||= "#{a.key};#{x.key};#{mem.map(&:key).join(',')};#{path.map(&:key).join(',')}"
end

#pinned(offset) ⇒ Integer?

The constant the data word at byte offset is pinned to on this path (by an == fact), or nil when it is not pinned.

Parameters:

  • offset (Integer)

Returns:

  • (Integer?) 


65
66
67
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 65

def pinned(offset)
  path.find { |c| c.plain_data_eq?(offset) }&.rhs&.val
end

#with(a: @a, x: @x, mem: @mem, path: @path) ⇒ State

Returns a copy with the given fields replaced; unreplaced fields are shared (the state is immutable).

Returns:



47
48
49
 
# File 'lib/seccomp-tools/symbolic/state.rb', line 47

def with(a: @a, x: @x, mem: @mem, path: @path)
  State.new(a:, x:, mem:, path:)
end