Class: Ibex::Verify::LanguageWitness::Machine

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

Overview

A stack machine shared by the canonical reference and submitted IR.

Instance Method Summary collapse

Constructor Details

#initialize(states, grammar) ⇒ Machine

Returns a new instance of Machine.

RBS:

  • (Array[IR::AutomatonState] states, IR::Grammar grammar) -> void

Parameters:



243
244
245
246
247
 
# File 'lib/ibex/verify/language_witness.rb', line 243

def initialize(states, grammar)
  @states = states
  @grammar = grammar
  @eof = grammar.symbol("$eof") || raise(Ibex::Error, "missing $eof terminal")
end

Instance Method Details

#consume(stack, token_id) ⇒ witness_status

RBS:

  • (Array[Integer], Integer) -> witness_status

Parameters:

  • (Array[Integer])
  • (Integer)

Returns:

  • (witness_status) 


266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
 
# File 'lib/ibex/verify/language_witness.rb', line 266

def consume(stack, token_id)
  steps = 0
  loop do
    steps += 1
    return :error if steps > 10_000

    state = @states.fetch(stack.last)
    action = state.actions.fetch(token_id, state.default_action || { type: :error })
    case action.fetch(:type)
    when :shift
      stack << action.fetch(:state)
      return :shifted
    when :reduce
      production = @grammar.productions.fetch(action.fetch(:production))
      return :error if production.rhs.length >= stack.length

      production.rhs.length.times { stack.pop }
      goto = @states.fetch(stack.last).gotos[production.lhs]
      return :error unless goto

      stack << goto
    when :accept then return :accepted
    else return :error
    end
  end
end

#simulate(initial, tokens) ⇒ witness_status

RBS:

  • (Integer initial, Array[Integer]) -> witness_status

Parameters:

  • initial (Integer)
  • (Array[Integer])

Returns:

  • (witness_status) 


250
251
252
253
254
255
256
257
258
259
260
261
 
# File 'lib/ibex/verify/language_witness.rb', line 250

def simulate(initial, tokens)
  stack = [initial]
  tokens.each do |token_id|
    status = consume(stack, token_id)
    return status unless status == :shifted
  end
  loop do
    status = consume(stack, @eof.id)
    return :accepted if status == :accepted
    return :error unless status == :shifted
  end
end