Module: Rigor::Effects::Narrowing

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

Overview

Argument-dependent narrowing for catalogue rows (ADR-103 WD3; the row's narrow: names one of these handlers, and data/effects/core.yml says why each row wants one).

A handler reads the call's own argument literals and nothing else. There is no dataflow here on purpose: the effect scan is observational (it never asks the typer for anything it did not already decide), and a narrowing that depended on inference would make the catalogue's answer a function of analysis quality rather than of the source in front of it.

Every handler is total and answers an upper bound: when the literal does not settle the question it returns the row's parent label, never a guess. open(path) with a computed argument is io — file, pipe or URI — and that is the honest reading of the classic pipe-injection shape.

Handlers are module functions dispatched by a case, deliberately not a Hash of lambdas: the catalogue is loaded once per process and inherited across the fork pool, and a table of procs is neither Marshal-clean nor shareable.

Constant Summary collapse

IO_ANY = 
LabelSet.new(["io"]).freeze
FS = 
LabelSet.new(["io.fs"]).freeze
FS_READ = 
LabelSet.new(["io.fs.read"]).freeze
FS_WRITE = 
LabelSet.new(["io.fs.write"]).freeze
FS_READ_WRITE = 
LabelSet.new(["io.fs.read", "io.fs.write"]).freeze
PROCESS = 
LabelSet.new(["io.process"]).freeze
HTTP = 
LabelSet.new(["io.net.http"]).freeze
TIME = 
LabelSet.new(["nondet.time"]).freeze
DB = 
LabelSet.new(["io.db"]).freeze
DB_READ = 
LabelSet.new(["io.db.read"]).freeze
DB_WRITE = 
LabelSet.new(["io.db.write"]).freeze
DB_TRANSACTION = 
LabelSet.new(["io.db.transaction"]).freeze
RANDOM = 
LabelSet.new(["nondet.random"]).freeze
NONE = 
LabelSet::EMPTY
HANDLERS = 
%w[kernel_open file_open pathname_open time_new random_new uri_open sql_verb].freeze

Class Method Summary collapse

Class Method Details

.apply(name, node) ⇒ Object

The labels name's handler reads off node. An unknown handler name answers nil, which the catalogue loader rejects at load time rather than at call time.



65
66
67
68
69
70
71
72
73
74
75
 
# File 'lib/rigor/effects/narrowing.rb', line 65

def apply(name, node)
  case name
  when "kernel_open" then kernel_open(node)
  when "file_open" then file_open(node)
  when "pathname_open" then pathname_open(node)
  when "time_new" then time_new(node)
  when "random_new" then random_new(node)
  when "uri_open" then uri_open(node)
  when "sql_verb" then sql_verb(node)
  end
end

.file_open(node) ⇒ Object

File.open(path, mode) — the mode literal decides the direction. An ABSENT mode is not an unknown one: Ruby's default is "r", so it reads. A mode the call computes — or an integer flag such as File::RDWR, which the scan deliberately does not resolve — is genuinely unknown and answers the subsystem parent.



113
114
115
 
# File 'lib/rigor/effects/narrowing.rb', line 113

def file_open(node)
  mode_labels(node, 1)
end

.kernel_open(node) ⇒ Object

Kernel#open — a path, a |command pipe, or (with open-uri loaded) a URI. A literal leading | is the pipe form; anything else literal is a path, whose direction the mode literal decides.



101
102
103
104
105
106
107
 
# File 'lib/rigor/effects/narrowing.rb', line 101

def kernel_open(node)
  target = literal_prefix(argument(node, 0))
  return IO_ANY if target.nil?
  return PROCESS if target.start_with?("|")

  mode_labels(node, 1)
end

.known?(name) ⇒ Boolean

Returns:

  • (Boolean) 


59
60
61
 
# File 'lib/rigor/effects/narrowing.rb', line 59

def known?(name)
  HANDLERS.include?(name)
end

.pathname_open(node) ⇒ Object

Pathname#open(mode) — the same reading one argument to the left, because the receiver is the path.



119
120
121
 
# File 'lib/rigor/effects/narrowing.rb', line 119

def pathname_open(node)
  mode_labels(node, 0)
end

.random_new(node) ⇒ Object

Random.new — a seed argument makes the generator reproducible from the source; without one it draws the seed from platform entropy.



131
132
133
 
# File 'lib/rigor/effects/narrowing.rb', line 131

def random_new(node)
  positional_count(node).zero? ? RANDOM : NONE
end

.time_new(node) ⇒ Object

Time.new — with no positional arguments it is Time.now; with any it constructs from them and consults no clock. Keyword arguments (in:) do not count: Time.new(in: "+09:00") is still now.



125
126
127
 
# File 'lib/rigor/effects/narrowing.rb', line 125

def time_new(node)
  positional_count(node).zero? ? TIME : NONE
end

.uri_open(node) ⇒ Object

URI.open / OpenURI.open_uri — the scheme literal decides the subsystem. A bare path (no scheme://) is open-uri's filesystem fallback; a scheme nobody rowed answers the parent.



137
138
139
140
141
142
143
144
145
 
# File 'lib/rigor/effects/narrowing.rb', line 137

def uri_open(node)
  target = literal_prefix(argument(node, 0))
  return IO_ANY if target.nil?
  return HTTP if target.start_with?("http://", "https://")
  return FS_READ if target.start_with?("file://")
  return IO_ANY if target.include?("://")

  FS_READ
end