Module: Rigor::Inference::IndexedNarrowing

Defined in:
lib/rigor/inference/indexed_narrowing.rb

Overview

Closes the “‘params ||= []; params << x`” precision gap surfaced by the Redmine 6.1.2 `Query#as_params` survey (ROADMAP § Future cycles / Type-language / engine —“Indexed-collection narrowing through `Hash ||= default`”).

After ‘receiver ||= default` the next read at `receiver` is known non-nil, but Rigor types each `Hash#[]` independently and the subsequent `<<` / `[]=` / other mutator dispatches against the un-narrowed result —which on a `HashShape{}` carrier folds to `Constant`.

This module is the address-recogniser + invalidator shared by StatementEvaluator‘s `eval_index_or_write` handler (which RECORDS the narrowing) and `eval_call` (which INVALIDATES on intervening writes / mutators) and by ExpressionTyper’s ‘call_type_for` (which CONSUMES the narrowing when typing a follow-up `[]` read).

**Stable receivers.** A receiver is “stable” iff it is a ‘LocalVariableReadNode` or `InstanceVariableReadNode`. Method-call chains (`foo.bar`) and other shapes are rejected because a follow-up read against an identical- looking AST chain has no guarantee of resolving to the same runtime value — narrowing it would invent a fact.

**Stable keys.** A key is “stable” iff it is a literal ‘SymbolNode` / `StringNode` / `IntegerNode`. Local-variable keys (`params`) are excluded for the same invent-a-fact reason: the local could be rebound between the `||=` and the read.

Invalidation. Three conditions drop a recorded narrowing:

  • The receiver variable is rebound (handled inside ‘Scope#with_local` / `Scope#with_ivar`).

  • An intervening ‘receiver = value` writes the same slot — `:[]=` could rebind the slot to nil; conservative drop.

  • An intervening mutator from MutationWidening::HASH_MUTATORS or MutationWidening::ARRAY_MUTATORS runs against the receiver (e.g. ‘params.delete(:f)`, `params.clear`).

All three are implemented in ‘StatementEvaluator#eval_call`’s post-dispatch path through IndexedNarrowing.invalidate_after_call.

Constant Summary collapse

STABLE_KEY_NODES =

Literal Prism nodes whose Ruby value the analyzer trusts as a stable address. Symbol / String are the dominant Hash key shapes; Integer covers numerically-keyed Hashes and Array indices.

[Prism::SymbolNode, Prism::StringNode, Prism::IntegerNode].freeze

Class Method Summary collapse

Class Method Details

.invalidate_after_call(call_node:, current_scope:) ⇒ Object

Removes recorded narrowings invalidated by ‘call_node`. Two patterns:

  • ‘receiver = value` (a `:[]=` against a stable address): drop the specific `(receiver, key)` entry.

  • Any mutator from ‘HASH_MUTATORS` / `ARRAY_MUTATORS` against a stable receiver: drop EVERY entry rooted at that receiver, because the mutator could rebind any slot.

Returns the updated scope. Always-safe (only forgets; never invents).



130
131
132
133
134
135
136
137
138
139
140
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 130

def invalidate_after_call(call_node:, current_scope:)
  return current_scope unless call_node.is_a?(Prism::CallNode)

  if call_node.name == :[]=
    invalidate_indexed_write(call_node, current_scope)
  elsif mutator?(call_node.name)
    invalidate_mutator(call_node, current_scope)
  else
    current_scope
  end
end

.invalidate_chain_after_call(call_node:, current_scope:) ⇒ Object

Companion invalidator for single-hop method-chain narrowings (ROADMAP § Future cycles — “Method-call receiver narrowing across stable receivers”, B2 from the slice’s design notes). Drops every ‘(receiver, *)` chain narrowing rooted at the call’s OUTER stable receiver — matching the ROADMAP’s “any intervening method call against the same receiver” criterion. A call against ‘x.last` (the OUTER receiver is a `CallNode`, not a stable root) does NOT drop narrowings keyed on `x`, so the worked-site `x.last << y` pattern correctly preserves the chain narrowing for any further `x.last` read in the same body. Always-safe (only forgets; never invents).



177
178
179
180
181
182
183
184
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 177

def invalidate_chain_after_call(call_node:, current_scope:)
  return current_scope unless call_node.is_a?(Prism::CallNode)

  receiver = stable_receiver(call_node.receiver)
  return current_scope if receiver.nil?

  current_scope.without_method_chain_narrowings_for(*receiver)
end

.invalidate_indexed_write(call_node, current_scope) ⇒ Object 



147
148
149
150
151
152
153
154
155
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 147

def invalidate_indexed_write(call_node, current_scope)
  args = call_node.arguments&.arguments
  return current_scope if args.nil? || args.empty?

  address = stable_address(call_node.receiver, args.first)
  return current_scope if address.nil?

  current_scope.without_indexed_narrowing(*address)
end

.invalidate_mutator(call_node, current_scope) ⇒ Object 



157
158
159
160
161
162
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 157

def invalidate_mutator(call_node, current_scope)
  receiver = stable_receiver(call_node.receiver)
  return current_scope if receiver.nil?

  current_scope.without_indexed_narrowings_for(*receiver)
end

.lookup_for_call(node, scope) ⇒ Object

Looks up a recorded narrowing for ‘receiver` against `scope`, returning the narrowed type or nil when no entry applies. Used by ExpressionTyper’s ‘[]` dispatch to refine the result of a stable indexed read.



106
107
108
109
110
111
112
113
114
115
116
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 106

def lookup_for_call(node, scope)
  return nil unless node.is_a?(Prism::CallNode)
  return nil unless node.name == :[]
  return nil if node.arguments.nil?
  return nil unless node.arguments.arguments.size == 1

  address = stable_address(node.receiver, node.arguments.arguments.first)
  return nil if address.nil?

  scope.indexed_narrowing(*address)
end

.mutator?(method_name) ⇒ Boolean

Returns:

  • (Boolean) 


142
143
144
145
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 142

def mutator?(method_name)
  MutationWidening::HASH_MUTATORS.include?(method_name) ||
    MutationWidening::ARRAY_MUTATORS.include?(method_name)
end

.stable_address(receiver_node, key_node) ⇒ Object

Returns ‘[receiver_kind, receiver_name, key]` when the CallNode is a `receiver` read or write whose receiver and key are both stable, otherwise nil. Used by both the recorder (for `IndexOrWriteNode`’s receiver/arguments triplet) and the invalidator (for ‘CallNode :[]=` / mutator calls). Treats only the FIRST argument as the key; `:[]=`’s second argument is the rvalue and is not part of the address.



92
93
94
95
96
97
98
99
100
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 92

def stable_address(receiver_node, key_node)
  receiver = stable_receiver(receiver_node)
  return nil if receiver.nil?

  key = stable_key(key_node)
  return nil if key.nil?

  [receiver.first, receiver.last, key]
end

.stable_key(node) ⇒ Object

Returns the literal Ruby value when ‘node` is a stable key shape, otherwise nil. Symbols → `Symbol`, Strings → `String` (unescaped), Integers → `Integer`.



76
77
78
79
80
81
82
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 76

def stable_key(node)
  case node
  when Prism::SymbolNode then node.unescaped.to_sym
  when Prism::StringNode then node.unescaped
  when Prism::IntegerNode then node.value
  end
end

.stable_receiver(node) ⇒ Object

Returns ‘[receiver_kind, receiver_name]` when `node` is a `LocalVariableReadNode` or `InstanceVariableReadNode`, otherwise nil.



66
67
68
69
70
71
 
# File 'lib/rigor/inference/indexed_narrowing.rb', line 66

def stable_receiver(node)
  case node
  when Prism::LocalVariableReadNode then [:local, node.name]
  when Prism::InstanceVariableReadNode then [:ivar, node.name]
  end
end