Module: Rigor::Effects::LocalOwnership

Defined in:
lib/rigor/effects/local_ownership.rb

Overview

Which of a method body's locals the frame owns — freshly allocated here and never let out (ADR-103 WD4; the proof obligations are control-flow-analysis.md § Proof obligations).

Ruby has no by-ref parameters, so mutate.local cannot mean "a write into an out-parameter" as it does in PHP. It means the mutated receiver is invisible to the caller, and that is an ownership question: a local whose every assignment allocates ([], {}, "", .new, .dup) and which never escapes the body is one no caller can observe being mutated.

The analysis is deliberately flow-insensitive and whole-body: a local that escapes anywhere disqualifies, even if the escape happens after the mutation. That is strictly more conservative than the "escaped before the mutating call" reading, which is the direction false positives are budgeted in (ADR-5) — an unproven local mutation becomes an unknown-ownership taint, never a proven mutate label.

This is the tracer slice's approximation, not the eventual answer. ClosureEscapeAnalyzer answers a different question (fact retention, not "does the code contain") and is deliberately left alone.

Constant Summary collapse

ALLOCATING_SELECTORS =

Assignment right-hand sides that witness a fresh allocation. .new and .dup / .clone follow ADR-76's reading of dup as the allocation witness.

%i[new dup clone].to_set.freeze

Class Method Summary collapse

Class Method Details

.allocation?(node) ⇒ Boolean

Whether node is an expression that allocates a fresh object this frame is the sole holder of.

Returns:

  • (Boolean) 


50
51
52
53
54
55
56
57
58
59
60
 
# File 'lib/rigor/effects/local_ownership.rb', line 50

def allocation?(node)
  case node
  when Prism::ArrayNode, Prism::HashNode, Prism::StringNode, Prism::InterpolatedStringNode,
       Prism::LambdaNode
    true
  when Prism::CallNode
    ALLOCATING_SELECTORS.include?(node.name) || unary_plus_string?(node)
  else
    false
  end
end

.owned(body, parameter_names) ⇒ Object

The set of frame-owned local names in body, given the method's parameter names (a parameter is never frame-owned — the caller holds the same object, so mutating it is mutate.instance).



35
36
37
38
39
40
41
42
43
44
45
46
47
 
# File 'lib/rigor/effects/local_ownership.rb', line 35

def owned(body, parameter_names)
  return Set.new if body.nil?

  assignments = {}
  escaped = Set.new
  collect(body, assignments, escaped)
  escaped.merge(trailing_reads(body))
  assignments.filter_map do |name, values|
    next if escaped.include?(name) || parameter_names.include?(name)

    name if values.all? { |value| allocation?(value) }
  end.to_set
end

.unary_plus_string?(node) ⇒ Boolean

+"" — the frozen-string-literal era's spelling of "a fresh mutable String".

Returns:

  • (Boolean) 


63
64
65
 
# File 'lib/rigor/effects/local_ownership.rb', line 63

def unary_plus_string?(node)
  node.name == :+@ && node.receiver.is_a?(Prism::StringNode)
end