Class: Ibex::Verify::Verifier

Inherits:
Object
  • Object
show all
Defined in:
lib/ibex/verify/verifier.rb,
sig/ibex/verify/verifier.rbs

Overview

Checks Automaton IR semantics against an independently derived collection. rubocop:disable Metrics/ClassLength -- V1-V9 share one violation and item-identity model.

Constant Summary collapse

DEFAULT_CHECKS =

Signature:

  • Array[String]

Returns:

  • (Array[String]) 
%w[V1 V3 V4 V6 V7 V8].freeze
STRICT_CHECKS =

Signature:

  • Array[String]

Returns:

  • (Array[String]) 
%w[V2 V5 V9].freeze
ERROR_ACTION =

Signature:

  • IR::error_action

Returns:

  • (IR::error_action) 
{ type: :error }.freeze

Instance Method Summary collapse

Constructor Details

#initialize(automaton, strict: false, max_states: 100_000, max_items: 1_000_000) ⇒ Verifier

Returns a new instance of Verifier.

RBS:

  • (IR::Automaton automaton, ?strict: bool, ?max_states: Integer, ?max_items: Integer) -> void

Parameters:

  • automaton (IR::Automaton)
  • strict: (Boolean) (defaults to: false)
  • max_states: (Integer) (defaults to: 100_000)
  • max_items: (Integer) (defaults to: 1_000_000) 


14
15
16
17
18
19
20
21
22
 
# File 'lib/ibex/verify/verifier.rb', line 14

def initialize(automaton, strict: false, max_states: 100_000, max_items: 1_000_000)
  @automaton = automaton
  @grammar = automaton.grammar
  @strict = strict
  @max_states = max_states
  @max_items = max_items
  @violations = [] #: Array[Violation]
  @sets = Analysis::Sets.new(@grammar)
end

Instance Method Details

#action_candidates(state) ⇒ Hash[Integer, Array[IR::parser_action]]

RBS:

  • (IR::AutomatonState state) -> Hash[Integer, Array[IR::parser_action]]

Parameters:

Returns:

  • (Hash[Integer, Array[IR::parser_action]]) 


427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
 
# File 'lib/ibex/verify/verifier.rb', line 427

def action_candidates(state)
  candidates = Hash.new { |hash, key| hash[key] = [] } #: Hash[Integer, Array[IR::parser_action]]
  state.transitions.each do |symbol_id, target|
    symbol = @grammar.symbol_by_id(symbol_id)
    candidates[symbol_id] << { type: :shift, state: target } if symbol&.terminal?
  end
  state.items.each do |item|
    next unless item.dot == rhs_for(item.production).length

    item.lookaheads.each do |lookahead|
      action = if item.production.negative?
                 { type: :accept } #: IR::accept_action
               else
                 { type: :reduce, production: item.production } #: IR::reduce_action
               end
      candidates[lookahead] << action
    end
  end
  candidates
end

#action_row(table, row) ⇒ Hash[Integer, IR::runtime_action]

RBS:

  • (Tables::action_table table, Integer row) -> Hash[Integer, IR::runtime_action]

Parameters:

  • table (Tables::action_table)
  • row (Integer)

Returns:

  • (Hash[Integer, IR::runtime_action]) 


316
317
318
 
# File 'lib/ibex/verify/verifier.rb', line 316

def action_row(table, row)
  table.is_a?(Array) ? table.fetch(row) : table.row(row)
end

#canonical_lr1_states ⇒ Array[Set[Array[Integer]]]

RBS:

  • () -> Array[Set[Array[Integer]]]

Returns:

  • (Array[Set[Array[Integer]]]) 


154
155
156
 
# File 'lib/ibex/verify/verifier.rb', line 154

def canonical_lr1_states
  reference.build(:lr1).states
end

#compare_expected_states(expected_states) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[Set[Array[Integer]]] expected_states) -> void

Parameters:

  • expected_states (Array[Set[Array[Integer]]]) 


159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
 
# File 'lib/ibex/verify/verifier.rb', line 159

def compare_expected_states(expected_states)
  expected_by_core = expected_states.group_by { |state| core_key(state) }
  matched = [] #: Array[Set[Array[Integer]]]
  @automaton.states.each do |state|
    actual = expanded_items(state)
    candidates = expected_by_core.fetch(core_key(actual), [])
    expected = candidates.find { |candidate| actual.subset?(candidate) }
    unless expected
      violation("V1", state_path(state), "item set is not a subset of an independently derived state")
      next
    end

    matched << expected
    missing = expected - actual
    violation("V2", state_path(state), "item set is missing #{missing.length} derived items") if
      @strict && !missing.empty?
  end
  return unless @strict

  expected_counts = multiset(expected_states)
  actual_counts = multiset(matched)
  return if expected_counts == actual_counts

  violation("V2", "$.states", "state collection is incomplete or contains duplicate derived states")
end

#compare_ielr_states(expected_states) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[Set[Array[Integer]]] expected_states) -> void

Parameters:

  • expected_states (Array[Set[Array[Integer]]]) 


186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
 
# File 'lib/ibex/verify/verifier.rb', line 186

def compare_ielr_states(expected_states)
  expected_by_core = expected_states.to_h { |state| [core_key(state), state] }
  actual_by_core = {} #: Hash[Array[Array[Integer]], Set[Array[Integer]]]
  @automaton.states.each do |state|
    actual = expanded_items(state)
    core = core_key(actual)
    expected = expected_by_core[core]
    unless expected && actual.subset?(expected)
      violation("V1", state_path(state), "IELR state contains an item outside its canonical-core union")
      next
    end
    merged = actual_by_core[core] ||= Set.new
    actual.each { |item| merged << item }
  end
  return unless @strict

  expected_by_core.each do |core, expected|
    next if actual_by_core.fetch(core, Set.new) == expected

    violation("V2", "$.states", "IELR partitions do not cover canonical lookaheads for core #{core.inspect}")
  end
end

#compare_slr_states(expected_states) ⇒ void

This method returns an undefined value.

SLR lookaheads affect completed items only. The builder may retain propagation lookaheads on non-completed items, but they cannot select an ACTION cell and therefore are outside the SLR semantic contract.

RBS:

  • (Array[Set[Array[Integer]]] expected_states) -> void

Parameters:

  • expected_states (Array[Set[Array[Integer]]]) 


100
101
102
103
104
105
106
107
108
109
110
111
112
113
 
# File 'lib/ibex/verify/verifier.rb', line 100

def compare_slr_states(expected_states)
  expected_by_core = expected_states.group_by { |state| state.to_a.sort }
  matched_cores = [] #: Array[Array[Array[Integer]]]
  @automaton.states.each do |state|
    core = verify_slr_state(state, expected_by_core)
    matched_cores << core if core
  end
  return unless @strict

  expected_cores = expected_states.map { |state| state.to_a.sort }
  return if matched_cores.sort == expected_cores.sort

  violation("V2", "$.states", "SLR state collection is incomplete or contains duplicate LR(0) cores")
end

#conflict_candidates(conflict) ⇒ Array[IR::parser_action]

RBS:

  • (IR::conflict conflict) -> Array[IR::parser_action]

Parameters:

  • conflict (IR::conflict)

Returns:

  • (Array[IR::parser_action]) 


400
401
402
403
404
405
406
407
408
409
410
411
 
# File 'lib/ibex/verify/verifier.rb', line 400

def conflict_candidates(conflict)
  if conflict.fetch(:type).to_sym == :shift_reduce
    shift_reduce = conflict #: IR::shift_reduce_conflict
    [
      { type: :shift, state: shift_reduce.fetch(:shift_to) },
      { type: :reduce, production: shift_reduce.fetch(:reduce) }
    ]
  else
    reduce_reduce = conflict #: IR::reduce_reduce_conflict
    reduce_reduce.fetch(:reductions).map { |production| { type: :reduce, production: production } }
  end
end

#core_key(state) ⇒ Array[Array[Integer]]

RBS:

  • (Set[Array[Integer]] state) -> Array[Array[Integer]]

Parameters:

  • state (Set[Array[Integer]])

Returns:

  • (Array[Array[Integer]]) 


541
542
543
 
# File 'lib/ibex/verify/verifier.rb', line 541

def core_key(state)
  state.map { |item| [item.fetch(0), item.fetch(1)] }.uniq.sort
end

#directed_cycle?(edges) ⇒ Boolean

RBS:

  • (Hash[Integer, Integer] edges) -> bool

Parameters:

  • edges (Hash[Integer, Integer])

Returns:

  • (Boolean) 


507
508
509
510
511
512
513
514
515
516
517
518
519
 
# File 'lib/ibex/verify/verifier.rb', line 507

def directed_cycle?(edges)
  edges.each_key do |start|
    seen = Set.new
    cursor = start
    while cursor && edges.key?(cursor)
      return true if seen.include?(cursor)

      seen << cursor
      cursor = edges[cursor]
    end
  end
  false
end

#effective_action(state, terminal_id) ⇒ IR::parser_action

RBS:

  • (IR::AutomatonState state, Integer terminal_id) -> IR::parser_action

Parameters:

Returns:

  • (IR::parser_action) 


463
464
465
 
# File 'lib/ibex/verify/verifier.rb', line 463

def effective_action(state, terminal_id)
  state.actions.fetch(terminal_id, state.default_action || ERROR_ACTION)
end

#eof_id ⇒ Integer

RBS:

  • () -> Integer

Returns:

  • (Integer) 


572
573
574
 
# File 'lib/ibex/verify/verifier.rb', line 572

def eof_id
  @grammar.symbol("$eof")&.id || raise(Ibex::Error, "(verify):1:1: grammar has no $eof terminal")
end

#expanded_items(state) ⇒ Set[Array[Integer]]

RBS:

  • (IR::AutomatonState state) -> Set[Array[Integer]]

Parameters:

Returns:

  • (Set[Array[Integer]]) 


522
523
524
525
526
 
# File 'lib/ibex/verify/verifier.rb', line 522

def expanded_items(state)
  state.items.each_with_object(Set.new) do |item, result|
    item.lookaheads.each { |lookahead| result << [item.production, item.dot, lookahead] }
  end
end

#follow_ids(production_id) ⇒ Array[Integer]

RBS:

  • (Integer production_id) -> Array[Integer]

Parameters:

  • production_id (Integer)

Returns:

  • (Array[Integer]) 


551
552
553
554
555
 
# File 'lib/ibex/verify/verifier.rb', line 551

def follow_ids(production_id)
  production = @grammar.productions.fetch(production_id)
  names = @sets.follow(production.lhs)
  names.map { |name| @grammar.symbol(name)&.id }.compact
end

#goto_row(table, row) ⇒ Hash[Integer, untyped]

RBS:

  • (Tables::goto_table table, Integer row) -> Hash[Integer, untyped]

Parameters:

  • table (Tables::goto_table)
  • row (Integer)

Returns:

  • (Hash[Integer, untyped]) 


321
322
323
 
# File 'lib/ibex/verify/verifier.rb', line 321

def goto_row(table, row)
  table.is_a?(Array) ? table.fetch(row) : table.row(row)
end

#lalr_states ⇒ Array[Set[Array[Integer]]]

RBS:

  • () -> Array[Set[Array[Integer]]]

Returns:

  • (Array[Set[Array[Integer]]]) 


145
146
147
148
149
150
151
 
# File 'lib/ibex/verify/verifier.rb', line 145

def lalr_states
  groups = canonical_lr1_states.group_by { |state| core_key(state) }
  groups.values.map do |states|
    merged = states.each_with_object(Set.new) { |state, result| state.each { |item| result << item } }
    visible_state(merged)
  end
end

#lr1_states ⇒ Array[Set[Array[Integer]]]

RBS:

  • () -> Array[Set[Array[Integer]]]

Returns:

  • (Array[Set[Array[Integer]]]) 


140
141
142
 
# File 'lib/ibex/verify/verifier.rb', line 140

def lr1_states
  canonical_lr1_states.map { |state| visible_state(state) }
end

#multiset(states) ⇒ Hash[Array[Array[Integer]], Integer]

RBS:

  • (Array[Set[Array[Integer]]] states) -> Hash[Array[Array[Integer]], Integer]

Parameters:

  • states (Array[Set[Array[Integer]]])

Returns:

  • (Hash[Array[Array[Integer]], Integer]) 


546
547
548
 
# File 'lib/ibex/verify/verifier.rb', line 546

def multiset(states)
  states.each_with_object(Hash.new(0)) { |state, counts| counts[state.to_a.sort] += 1 }
end

#productive_nonterminals ⇒ Set[Integer]

RBS:

  • () -> Set[Integer]

Returns:

  • (Set[Integer]) 


487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
 
# File 'lib/ibex/verify/verifier.rb', line 487

def productive_nonterminals
  productive = Set.new
  pending = @grammar.productions.dup
  loop do
    changed = false
    pending.delete_if do |production|
      ready = production.rhs.all? do |id|
        symbol = @grammar.symbol_by_id(id)
        symbol&.terminal? || productive.include?(id)
      end
      productive << production.lhs if ready
      changed ||= ready
      ready
    end
    break unless changed
  end
  productive
end

#reachable_states ⇒ Set[Integer]

RBS:

  • () -> Set[Integer]

Returns:

  • (Set[Integer]) 


468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
 
# File 'lib/ibex/verify/verifier.rb', line 468

def reachable_states
  found = Set.new
  queue = @automaton.entry_states.values.dup
  until queue.empty?
    id = queue.shift
    next if found.include?(id)

    found << id
    state = @automaton.states[id]
    next unless state

    queue.concat(state.transitions.values)
    queue.concat(state.gotos.values)
    state.actions.each_value { |action| queue << action[:state] if action[:type] == :shift }
  end
  found
end

#reference ⇒ ReferenceCollection

RBS:

  • () -> ReferenceCollection

Returns:



584
585
586
 
# File 'lib/ibex/verify/verifier.rb', line 584

def reference
  @reference ||= ReferenceCollection.new(@grammar, max_states: @max_states, max_items: @max_items)
end

#resolved_conflict_action(conflict) ⇒ IR::parser_action?

RBS:

  • (IR::conflict conflict) -> IR::parser_action?

Parameters:

  • conflict (IR::conflict)

Returns:

  • (IR::parser_action, nil) 


414
415
416
417
418
419
420
421
422
423
424
 
# File 'lib/ibex/verify/verifier.rb', line 414

def resolved_conflict_action(conflict)
  chosen = conflict.fetch(:resolution).fetch(:chose)
  return { type: :reduce, production: chosen } if chosen.is_a?(Integer) #: IR::reduce_action

  shift_reduce = conflict #: IR::shift_reduce_conflict
  case chosen.to_sym
  when :shift then { type: :shift, state: shift_reduce.fetch(:shift_to) }
  when :reduce then { type: :reduce, production: shift_reduce.fetch(:reduce) }
  when :error then ERROR_ACTION
  end
end

#rhs_for(production_id) ⇒ Array[Integer]

RBS:

  • (Integer production_id) -> Array[Integer]

Parameters:

  • production_id (Integer)

Returns:

  • (Array[Integer]) 


558
559
560
561
562
563
 
# File 'lib/ibex/verify/verifier.rb', line 558

def rhs_for(production_id)
  return [start_symbol(production_id).id] if production_id.negative?

  production = @grammar.productions[production_id]
  production&.rhs || []
end

#shifted_items(state, symbol_id) ⇒ Array[Array[Integer]]

RBS:

  • (IR::AutomatonState state, Integer symbol_id) -> Array[Array[Integer]]

Parameters:

Returns:

  • (Array[Array[Integer]]) 


449
450
451
452
453
454
455
456
457
458
459
460
 
# File 'lib/ibex/verify/verifier.rb', line 449

def shifted_items(state, symbol_id)
  state.items.filter_map do |item|
    expected_symbol = rhs_for(item.production)[item.dot]
    if item.production.negative? && item.dot.zero?
      next unless start_symbol_ids.include?(symbol_id)
    else
      next unless expected_symbol == symbol_id
    end

    item.lookaheads.map { |lookahead| [item.production, item.dot + 1, lookahead] }
  end.flatten(1)
end

#start_symbol(production_id) ⇒ IR::GrammarSymbol

RBS:

  • (Integer production_id) -> IR::GrammarSymbol

Parameters:

  • production_id (Integer)

Returns:



566
567
568
569
 
# File 'lib/ibex/verify/verifier.rb', line 566

def start_symbol(production_id)
  name = @grammar.starts.fetch(-production_id - 1)
  @grammar.symbol(name) || raise(Ibex::Error, "(verify):1:1: missing start symbol #{name}")
end

#start_symbol_ids ⇒ Array[Integer]

RBS:

  • () -> Array[Integer]

Returns:

  • (Array[Integer]) 


577
578
579
580
581
 
# File 'lib/ibex/verify/verifier.rb', line 577

def start_symbol_ids
  @start_symbol_ids ||= @grammar.starts.map do |name|
    @grammar.symbol(name)&.id || raise(Ibex::Error, "(verify):1:1: missing start symbol #{name}")
  end
end

#state_path(state) ⇒ String

RBS:

  • (IR::AutomatonState state) -> String

Parameters:

Returns:

  • (String) 


594
 
# File 'lib/ibex/verify/verifier.rb', line 594

def state_path(state) = "$.states[#{state.id}]"

#verify ⇒ Result

RBS:

  • () -> Result

Returns:



25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
 
# File 'lib/ibex/verify/verifier.rb', line 25

def verify
  @violations.clear
  verify_grammar_digest
  verify_item_collection
  verify_transitions_and_actions
  verify_table_formats
  verify_reachability_and_productivity
  verify_epsilon_termination
  verify_conflict_determinism
  verify_ielr_adequacy if @strict
  Result.new(
    algorithm: @automaton.algorithm, strict: @strict,
    checks: DEFAULT_CHECKS + (@strict ? STRICT_CHECKS : []),
    violations: @violations,
    bounds: { max_states: @max_states, max_items: @max_items }
  )
end

#verify_conflict_determinism ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
 
# File 'lib/ibex/verify/verifier.rb', line 365

def verify_conflict_determinism
  @automaton.states.each do |state|
    grouped = state.conflicts.group_by { |conflict| conflict.fetch(:symbol) }
    grouped.each do |symbol, conflicts|
      violation("V8", state_path(state), "#{symbol} has more than one declared resolver") if conflicts.length > 1
      resolution = conflicts.first&.fetch(:resolution, nil)
      unless resolution&.key?(:by) && resolution.key?(:chose)
        violation("V8", state_path(state), "#{symbol} has an incomplete resolver")
        next
      end

      verify_conflict_resolution(state, conflicts.first)
    end
  end
end

#verify_conflict_resolution(state, conflict) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::conflict conflict) -> void

Parameters:



382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
 
# File 'lib/ibex/verify/verifier.rb', line 382

def verify_conflict_resolution(state, conflict)
  terminal = @grammar.symbol(conflict.fetch(:symbol))
  unless terminal&.terminal?
    violation("V8", state_path(state), "resolver references a missing terminal")
    return
  end

  candidates = action_candidates(state).fetch(terminal.id, []).uniq
  expected = resolved_conflict_action(conflict)
  unless conflict_candidates(conflict).all? { |candidate| candidates.include?(candidate) }
    violation("V8", state_path(state), "#{terminal.name} resolver names actions outside the cell")
  end
  return if expected && effective_action(state, terminal.id) == expected

  violation("V8", state_path(state), "#{terminal.name} resolver choice does not match the ACTION cell")
end

#verify_conflicted_action(state, terminal, expected, actual, conflict_tokens) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::GrammarSymbol terminal, Array[IR::parser_action] expected, IR::parser_action actual, Array[Integer] conflict_tokens) -> void

Parameters:



287
288
289
290
291
292
293
294
 
# File 'lib/ibex/verify/verifier.rb', line 287

def verify_conflicted_action(state, terminal, expected, actual, conflict_tokens)
  unless expected.include?(actual) || actual[:type] == :error
    violation("V8", state_path(state), "#{terminal.name} selects an action outside its candidates")
  end
  return if conflict_tokens.include?(terminal.id)

  violation("V8", state_path(state), "#{terminal.name} has multiple actions without a declared resolver")
end

#verify_epsilon_termination ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
 
# File 'lib/ibex/verify/verifier.rb', line 345

def verify_epsilon_termination
  @grammar.terminals.each do |terminal|
    edges = {} #: Hash[Integer, Integer]
    @automaton.states.each do |state|
      action = effective_action(state, terminal.id)
      next unless action[:type] == :reduce

      production = @grammar.productions[action.fetch(:production)]
      next unless production&.rhs&.empty?

      target = state.gotos[production.lhs]
      edges[state.id] = target if target
    end
    next unless directed_cycle?(edges)

    violation("V7", "$.states", "epsilon reductions can cycle without consuming #{terminal.name}")
  end
end

#verify_error_cell(state, terminal, actual) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::GrammarSymbol terminal, IR::parser_action actual) -> void

Parameters:



270
271
272
273
274
 
# File 'lib/ibex/verify/verifier.rb', line 270

def verify_error_cell(state, terminal, actual)
  return if actual[:type] == :error

  violation("V4", state_path(state), "#{terminal.name} replaces an error cell with #{actual.inspect}")
end

#verify_grammar_digest ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



77
78
79
80
81
82
83
 
# File 'lib/ibex/verify/verifier.rb', line 77

def verify_grammar_digest
  require "digest"
  actual = "sha256:#{Digest::SHA256.hexdigest(IR::Serialize.dump(@grammar))}"
  return if actual == @automaton.grammar_digest

  violation("V1", "$.grammar_digest", "digest does not match the embedded Grammar IR")
end

#verify_ielr_adequacy ⇒ void

This method returns an undefined value.

V9 is a bounded semantic witness for IELR only. It deliberately does not replace V1/V2 or claim unbounded language equivalence.

RBS:

  • () -> void



48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
 
# File 'lib/ibex/verify/verifier.rb', line 48

def verify_ielr_adequacy
  return unless @automaton.algorithm == "ielr1"

  witness = LanguageWitness.new(
    @grammar, @automaton, max_tokens: 3, max_cases: 10_000,
                          max_states: @max_states, max_items: @max_items
  ).verify
  if witness.truncated
    violation(
      "V9", "$.states",
      "bounded canonical acceptance witness exhausted its budget " \
      "(max_tokens=#{witness.max_tokens}, max_cases=#{witness.max_cases})"
    )
  end
  witness.differences.each do |difference|
    violation(
      "V9", "$.states",
      "canonical/target acceptance differs for entry #{difference.entry.inspect} " \
      "and tokens #{difference.tokens.inspect}: " \
      "canonical=#{difference.canonical}, target=#{difference.target}"
    )
  end
rescue BudgetExceeded
  raise
rescue StandardError => e
  violation("V9", "$.states", "bounded canonical acceptance witness failed: #{e.message}")
end

#verify_item_collection ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



86
87
88
89
90
91
92
93
94
 
# File 'lib/ibex/verify/verifier.rb', line 86

def verify_item_collection
  case @automaton.algorithm
  when "slr" then compare_slr_states(reference.build(:lr0).states.map { |state| visible_state(state) })
  when "lalr1" then compare_expected_states(lalr_states)
  when "lr1" then compare_expected_states(lr1_states)
  when "ielr1" then compare_ielr_states(lalr_states)
  else violation("V1", "$.algorithm", "unsupported algorithm #{@automaton.algorithm.inspect}")
  end
end

#verify_reachability_and_productivity ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
 
# File 'lib/ibex/verify/verifier.rb', line 326

def verify_reachability_and_productivity
  reachable = reachable_states
  @automaton.states.each do |state|
    unless reachable.include?(state.id)
      violation("V6", state_path(state),
                "state is unreachable from every entry")
    end
  end

  productive = productive_nonterminals
  @grammar.nonterminals.each do |symbol|
    unless productive.include?(symbol.id)
      violation("V6", "$.grammar.symbols[#{symbol.id}]",
                "nonterminal #{symbol.name} derives no terminal sentence")
    end
  end
end

#verify_single_action(state, terminal, expected, actual) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::GrammarSymbol terminal, IR::parser_action expected, IR::parser_action actual) -> void

Parameters:



278
279
280
281
282
283
 
# File 'lib/ibex/verify/verifier.rb', line 278

def verify_single_action(state, terminal, expected, actual)
  return if actual == expected

  violation("V1", state_path(state),
            "#{terminal.name} selects #{actual.inspect}, expected #{expected.inspect}")
end

#verify_slr_lookaheads(state, item) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::AutomatonItem item) -> void

Parameters:



130
131
132
133
134
135
136
137
 
# File 'lib/ibex/verify/verifier.rb', line 130

def verify_slr_lookaheads(state, item)
  return unless item.dot == rhs_for(item.production).length

  expected = item.production.negative? ? [eof_id] : follow_ids(item.production)
  return if item.lookaheads == expected.sort

  violation("V3", state_path(state), "completed item #{item.production} has invalid SLR lookaheads")
end

#verify_slr_state(state, expected_by_core) ⇒ Array[Array[Integer]]?

RBS:

  • (IR::AutomatonState state, Hash[Array[Array[Integer]], Array[Set[Array[Integer]]]] expected_by_core) -> Array[Array[Integer]]?

Parameters:

  • state (IR::AutomatonState)
  • expected_by_core (Hash[Array[Array[Integer]], Array[Set[Array[Integer]]]])

Returns:

  • (Array[Array[Integer]], nil) 


118
119
120
121
122
123
124
125
126
127
 
# File 'lib/ibex/verify/verifier.rb', line 118

def verify_slr_state(state, expected_by_core)
  actual_core = state.items.map { |item| [item.production, item.dot] }.uniq.sort
  unless expected_by_core.key?(actual_core)
    violation("V1", state_path(state), "item core is not in the independently derived LR(0) collection")
    return
  end

  state.items.each { |item| verify_slr_lookaheads(state, item) }
  actual_core
end

#verify_state_actions(state) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state) -> void

Parameters:



241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
 
# File 'lib/ibex/verify/verifier.rb', line 241

def verify_state_actions(state)
  candidates = action_candidates(state)
  conflict_tokens = state.conflicts.filter_map do |conflict|
    @grammar.symbol(conflict.fetch(:symbol))&.id
  end
  if state.default_action && state.default_action[:type] != :reduce
    violation("V4", state_path(state), "default action must be a reduction")
  end

  @grammar.terminals.each do |terminal|
    expected = candidates.fetch(terminal.id, []).uniq
    actual = effective_action(state, terminal.id)
    verify_terminal_action(state, terminal, expected, actual, conflict_tokens)
  end
end

#verify_table_formats ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
 
# File 'lib/ibex/verify/verifier.rb', line 297

def verify_table_formats
  plain = Tables.build(@automaton, format: :plain)
  compact = Tables.build(@automaton, format: :compact)
  @automaton.states.each do |state|
    unless action_row(plain.actions, state.id) == action_row(compact.actions, state.id)
      violation(@strict ? "V5" : "V4", state_path(state), "plain/compact ACTION rows differ")
    end
    unless goto_row(plain.gotos, state.id) == goto_row(compact.gotos, state.id)
      violation(@strict ? "V5" : "V4", state_path(state), "plain/compact GOTO rows differ")
    end
    next if plain.default_actions.fetch(state.id) == compact.default_actions.fetch(state.id)

    violation(@strict ? "V5" : "V4", state_path(state), "plain/compact default actions differ")
  end
rescue StandardError => e
  violation(@strict ? "V5" : "V4", "$.states", "table transformation failed: #{e.message}")
end

#verify_terminal_action(state, terminal, expected, actual, conflict_tokens) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state, IR::GrammarSymbol terminal, Array[IR::parser_action] expected, IR::parser_action actual, Array[Integer] conflict_tokens) -> void

Parameters:



259
260
261
262
263
264
265
266
267
 
# File 'lib/ibex/verify/verifier.rb', line 259

def verify_terminal_action(state, terminal, expected, actual, conflict_tokens)
  if expected.empty?
    verify_error_cell(state, terminal, actual)
  elsif expected.one?
    verify_single_action(state, terminal, expected.fetch(0), actual)
  else
    verify_conflicted_action(state, terminal, expected, actual, conflict_tokens)
  end
end

#verify_transition_items(state) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::AutomatonState state) -> void

Parameters:



218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
 
# File 'lib/ibex/verify/verifier.rb', line 218

def verify_transition_items(state)
  state.transitions.each do |symbol_id, target_id|
    symbol = @grammar.symbol_by_id(symbol_id)
    target = @automaton.states[target_id]
    unless symbol && target
      violation("V1", state_path(state), "transition references a missing symbol or state")
      next
    end

    expected = shifted_items(state, symbol_id)
    actual = expanded_items(target)
    missing = expected.reject { |item| actual.include?(item) }
    unless missing.empty?
      violation("V1", state_path(state),
                "transition on #{symbol.name} loses #{missing.length} shifted items")
    end
    if symbol.nonterminal? && state.gotos[symbol_id] != target_id
      violation("V1", state_path(state), "nonterminal transition #{symbol.name} has no matching goto")
    end
  end
end

#verify_transitions_and_actions ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



210
211
212
213
214
215
 
# File 'lib/ibex/verify/verifier.rb', line 210

def verify_transitions_and_actions
  @automaton.states.each do |state|
    verify_transition_items(state)
    verify_state_actions(state)
  end
end

#violation(id, location, message) ⇒ void

This method returns an undefined value.

RBS:

  • (String id, String location, String message) -> void

Parameters:

  • id (String)
  • location (String)
  • message (String) 


589
590
591
 
# File 'lib/ibex/verify/verifier.rb', line 589

def violation(id, location, message)
  @violations << Violation.new(id: id, location: location, message: message).freeze
end

#visible_state(state) ⇒ Set[Array[Integer]]

Automaton IR intentionally exposes every augmented production as -1, even when construction internally assigned one per start symbol.

RBS:

  • (Set[Array[Integer]] state) -> Set[Array[Integer]]

Parameters:

  • state (Set[Array[Integer]])

Returns:

  • (Set[Array[Integer]]) 


531
532
533
534
535
536
537
538
 
# File 'lib/ibex/verify/verifier.rb', line 531

def visible_state(state)
  state.each_with_object(Set.new) do |item, result|
    production = item.fetch(0)
    dot = item.fetch(1)
    lookahead = item[2]
    result << [production.negative? ? -1 : production, dot, lookahead].compact
  end
end