Class: SeccompTools::Symbolic::Expr

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

Overview

A value the executor only knows symbolically - that is, without picking concrete inputs.

Every register and scratch slot in the State holds an Expr, which is one of:

  • Expr.imm - a known 32-bit constant, e.g. the result of A = 5.
  • Expr.data - a single word of the input data buffer, at some byte offset. Its value is unknown; we only remember where it was read from.
  • Expr.binop - an arithmetic combination of two sub-expressions, e.g. data[16] & 0xffff or even data[16] & data[24] (two buffer words combined). This is what lets a caller later describe a branch condition faithfully.
  • Expr.unop - a unary operation on a sub-expression; the only one BPF has is negation (+-A+).
  • Expr.opaque - a value we cannot describe (an unsupported operation, or one whose operand is itself opaque). Nothing can be concluded about it.

Constant Summary collapse

REPRESENTABLE =

The binary ALU operators #apply accepts - exactly the ones Instruction::ALU#symbolize can produce (its unary neg is handled separately).

Instruction::ALU::OP_SYM.values.freeze

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(kind, **fields) ⇒ Expr

Returns a new instance of Expr.

Parameters:

  • kind (:imm, :data, :binop, :unop, :opaque)
  • fields (Hash) —

    The kind-specific fields: :val, :offset, :op, :lhs, :rhs.



82
83
84
85
86
87
88
89
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 82

def initialize(kind, **fields)
  @kind = kind
  @val = fields[:val]
  @offset = fields[:offset]
  @op = fields[:op]
  @lhs = fields[:lhs]
  @rhs = fields[:rhs]
end

Instance Attribute Details

#kind ⇒ :imm, ... (readonly)

Returns Which kind of expression this is.

Returns:

  • (:imm, :data, :binop, :unop, :opaque) —

    Which kind of expression this is.



30
31
32
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 30

def kind
  @kind
end

#lhs ⇒ Expr? (readonly)

Returns The left and right operands, when kind is :binop; a :unop keeps its only operand in lhs.

Returns:

  • (Expr?) —

    The left and right operands, when kind is :binop; a :unop keeps its only operand in lhs.



39
40
41
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 39

def lhs
  @lhs
end

#offset ⇒ Integer? (readonly)

Returns The byte offset into the input data buffer, when kind is :data.

Returns:

  • (Integer?) —

    The byte offset into the input data buffer, when kind is :data.



34
35
36
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 34

def offset
  @offset
end

#op ⇒ Symbol? (readonly)

Returns The operator, when kind is :binop or :unop.

Returns:

  • (Symbol?) —

    The operator, when kind is :binop or :unop.



36
37
38
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 36

def op
  @op
end

#rhs ⇒ Expr? (readonly)

Returns The left and right operands, when kind is :binop; a :unop keeps its only operand in lhs.

Returns:

  • (Expr?) —

    The left and right operands, when kind is :binop; a :unop keeps its only operand in lhs.



39
40
41
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 39

def rhs
  @rhs
end

#val ⇒ Integer? (readonly)

Returns The constant, when kind is :imm.

Returns:

  • (Integer?) —

    The constant, when kind is :imm.



32
33
34
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 32

def val
  @val
end

Class Method Details

.binop(op, lhs, rhs) ⇒ Expr

An arithmetic combination of two expressions.

Parameters:

Returns:



61
62
63
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 61

def self.binop(op, lhs, rhs)
  new(:binop, op:, lhs:, rhs:)
end

.data(offset) ⇒ Expr

A single word of the input data buffer.

Parameters:

  • offset (Integer) —

    Byte offset into the buffer.

Returns:



52
53
54
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 52

def self.data(offset)
  new(:data, offset:)
end

.fold(lhs, op, rhs) ⇒ Integer

Folds a binary ALU operation on two constants, wrapping to 32 bits (classic BPF is 32-bit). Every REPRESENTABLE operator is a Ruby Integer method, so it applies directly.

Returns:

  • (Integer) 


161
162
163
164
165
166
167
168
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 161

def self.fold(lhs, op, rhs)
  return 0 if op == :/ && rhs.zero? # a real BPF program is rejected at load for div-by-zero
  # ... and for shifts of 32+ bits; short-circuit them to their masked result (everything
  # shifted out) instead of building a needlessly huge integer.
  return 0 if %i[<< >>].include?(op) && rhs >= 32

  lhs.public_send(op, rhs) & 0xffffffff
end

.imm(val) ⇒ Expr

A known constant.

Parameters:

  • val (Integer)

Returns:



44
45
46
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 44

def self.imm(val)
  new(:imm, val: val & 0xffffffff)
end

.opaque ⇒ Expr

A value that cannot be described symbolically.

Returns:



75
76
77
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 75

def self.opaque
  new(:opaque)
end

.unop(op, operand) ⇒ Expr

A unary operation on one expression (its operand is kept in lhs).

Parameters:

  • op (Symbol)
  • operand (Expr)

Returns:



69
70
71
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 69

def self.unop(op, operand)
  new(:unop, op:, lhs: operand)
end

Instance Method Details

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

Parameters:

Returns:

  • (Boolean) 


148
149
150
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 148

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

#apply(op, operand) ⇒ Expr

Applies an ALU operation, returning the resulting SeccompTools::Symbolic::Expr. neg is unary (its operand is ignored). Two constants fold into a new constant; an operation on non-opaque operands becomes a binop; an opaque operand makes the result opaque.

Parameters:

  • op (Symbol) —

    A Ruby operator symbol as produced by Instruction::ALU#symbolize, or :neg.

  • operand (Expr, nil) —

    The right operand (+nil+ for the unary neg).

Returns:

Raises:

  • (ArgumentError) —

    When op is not one of seccomp's ALU operators (+:neg+ or REPRESENTABLE).



118
119
120
121
122
123
124
125
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 118

def apply(op, operand)
  return apply_neg if op == :neg
  raise ArgumentError, "unsupported operator #{op}" unless REPRESENTABLE.include?(op)
  return Expr.opaque if opaque? || operand.opaque?
  return Expr.imm(self.class.fold(val, op, operand.val)) if imm? && operand.imm?

  Expr.binop(op, self, operand)
end

#hash ⇒ Integer

Returns:

  • (Integer) 


154
155
156
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 154

def hash
  key.hash
end

#imm? ⇒ Boolean

Returns:

  • (Boolean) 


92
93
94
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 92

def imm?
  kind == :imm
end

#key ⇒ String

A string that uniquely identifies this expression, used for both equality and hashing; memoized, since an SeccompTools::Symbolic::Expr is immutable. The operator is written as text, not left a Symbol, because Ruby's Symbol#hash maps the operators to very few values (+:==+ and :!= hash alike) - a key carrying them would collapse when hashed and drag the walk's visited Set down to a linear scan; a string hashes over its bytes cleanly. The encoding is injective (leaves are i<val> / d<offset> / o, compounds are parenthesised, and no operator contains a leaf-start char, a digit, or the ; / , that State joins with), so it is safe to compare on.

Returns:

  • (String) 


136
137
138
139
140
141
142
143
144
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 136

def key
  @key ||= case kind
           when :binop then "(#{lhs.key}#{op}#{rhs.key})"
           when :unop  then "(#{op}#{lhs.key})"
           when :imm   then "i#{val}"
           when :data  then "d#{offset}"
           else 'o'
           end
end

#opaque? ⇒ Boolean

Returns:

  • (Boolean) 


104
105
106
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 104

def opaque?
  kind == :opaque
end

#plain_data? ⇒ Boolean

Is this a bare data-buffer word (no arithmetic applied)? These are the values a caller can compare directly against a constant.

Returns:

  • (Boolean) 


99
100
101
 
# File 'lib/seccomp-tools/symbolic/expr.rb', line 99

def plain_data?
  kind == :data
end