Class: Ibex::Equiv

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

Overview

Bounded language comparison over two immutable parser automata. rubocop:disable Metrics/ClassLength -- the three comparison strategies share one report and budget contract.

Defined Under Namespace

Classes: BudgetExceeded, Difference, Machine

Constant Summary collapse

CAVEAT =

RBS:

  • type tree_node_signature = [String, Array[String]]
type tree_trace_entry = [String, Array[String], tree_node_signature?]
type terminal_signature = [String, [Symbol, Integer]?]
type production_signature = [String, Array[String], String?]

Returns:

  • (String) 
"Bounded search is not a proof of equivalence."
DEFAULT_MAX_ACTIONS =

Signature:

  • String

Returns:

  • (Integer) 
100_000
DEFAULT_MAX_STACK =

Signature:

  • Integer

Returns:

  • (Integer) 
10_000

Instance Method Summary collapse

Constructor Details

#initialize(left, right, sample_count: 100, seed: 0, max_tokens: 8, max_configurations: 50_000, max_actions: DEFAULT_MAX_ACTIONS, max_stack: DEFAULT_MAX_STACK, rule_map: {}) ⇒ Equiv

Returns a new instance of Equiv.

RBS:

  • (IR::Automaton left, IR::Automaton right, ?sample_count: Integer, ?seed: Integer, ?max_tokens: Integer, ?max_configurations: Integer, ?max_actions: Integer, ?max_stack: Integer, ?rule_map: Hash[String, String]) -> void

Parameters:

  • left (IR::Automaton)
  • right (IR::Automaton)
  • sample_count: (Integer) (defaults to: 100)
  • seed: (Integer) (defaults to: 0)
  • max_tokens: (Integer) (defaults to: 8)
  • max_configurations: (Integer) (defaults to: 50_000)
  • max_actions: (Integer) (defaults to: DEFAULT_MAX_ACTIONS)
  • max_stack: (Integer) (defaults to: DEFAULT_MAX_STACK)
  • rule_map: (Hash[String, String]) (defaults to: {}) 


46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
 
# File 'lib/ibex/equiv.rb', line 46

def initialize(left, right, sample_count: 100, seed: 0, max_tokens: 8, max_configurations: 50_000,
               max_actions: DEFAULT_MAX_ACTIONS, max_stack: DEFAULT_MAX_STACK, rule_map: {})
  budgets = {
    sample_count: sample_count, max_tokens: max_tokens, max_configurations: max_configurations,
    max_actions: max_actions, max_stack: max_stack
  }
  invalid = budgets.find { |_name, value| !value.positive? }
  raise ArgumentError, "#{invalid.fetch(0)} must be positive" if invalid

  @left = left
  @right = right
  @sample_count = sample_count
  @seed = seed
  @max_tokens = max_tokens
  @max_configurations = max_configurations
  @max_actions = max_actions
  @max_stack = max_stack
  @rule_map = rule_map.dup.freeze
  validate_rule_map!
  @left_machine = Machine.new(left, max_actions: max_actions, max_stack: max_stack)
  @right_machine = Machine.new(right, max_actions: max_actions, max_stack: max_stack)
end

Instance Method Details

#both_rejected?(left, right) ⇒ Boolean

RBS:

  • (Machine::Configuration left, Machine::Configuration right) -> bool

Parameters:

Returns:

  • (Boolean) 


331
332
333
 
# File 'lib/ibex/equiv.rb', line 331

def both_rejected?(left, right)
  left.status == :error && right.status == :error
end

#bounds ⇒ Hash[Symbol, Integer]

RBS:

  • () -> Hash[Symbol, Integer]

Returns:

  • (Hash[Symbol, Integer]) 


360
361
362
363
364
365
 
# File 'lib/ibex/equiv.rb', line 360

def bounds
  {
    sample_count: @sample_count, seed: @seed, max_tokens: @max_tokens,
    max_configurations: @max_configurations, max_actions: @max_actions, max_stack: @max_stack
  }
end

#compare_configurations!(left, right, tokens) ⇒ void

This method returns an undefined value.

RBS:

  • (Machine::Configuration left, Machine::Configuration right, Array[String] tokens) -> void

Parameters:



162
163
164
165
166
 
# File 'lib/ibex/equiv.rb', line 162

def compare_configurations!(left, right, tokens)
  left_result = @left_machine.finish(left)
  right_result = @right_machine.finish(right)
  compare_results!(left_result, right_result, tokens, "bounded_product_bfs")
end

#compare_results!(left, right, tokens, method) ⇒ void

This method returns an undefined value.

RBS:

  • (Machine::Configuration left, Machine::Configuration right, Array[String] tokens, String method) -> void

Parameters:



169
170
171
172
173
174
175
176
177
178
179
180
 
# File 'lib/ibex/equiv.rb', line 169

def compare_results!(left, right, tokens, method)
  raise_language_difference(tokens, left.status, right.status, method) unless left.status == right.status
  return unless left.status == :accepted && tree_requested?
  return if tree_trace(@left, left, map_left: true) == tree_trace(@right, right, map_left: false)

  raise Difference.new(
    ibex_report: "equiv", schema_version: 1, result: "difference",
    difference_kind: "tree", method: "#{method}_tree_trace", witness: tokens,
    outcomes: { left: left.status, right: right.status },
    bounds: bounds, statement: CAVEAT
  )
end

#compare_samples ⇒ Integer

RBS:

  • () -> Integer

Returns:

  • (Integer) 


97
98
99
100
101
102
103
 
# File 'lib/ibex/equiv.rb', line 97

def compare_samples
  left_samples = generated_samples(@left.grammar, @seed)
  right_samples = generated_samples(@right.grammar, @seed ^ 0x1BE)
  left_samples.each { |tokens| compare_tokens!(tokens, method: "left_to_right_sampling") }
  right_samples.each { |tokens| compare_tokens!(tokens, method: "right_to_left_sampling") }
  left_samples.length + right_samples.length
end

#compare_tokens!(tokens, method:) ⇒ void

This method returns an undefined value.

RBS:

  • (Array[String] tokens, method: String) -> void

Parameters:

  • tokens (Array[String])
  • method: (String) 


155
156
157
158
159
 
# File 'lib/ibex/equiv.rb', line 155

def compare_tokens!(tokens, method:)
  left = @left_machine.finish(@left_machine.run(tokens))
  right = @right_machine.finish(@right_machine.run(tokens))
  compare_results!(left, right, tokens, method)
end

#generated_samples(grammar, seed) ⇒ Array[Array[String]]

RBS:

  • (IR::Grammar grammar, Integer seed) -> Array[Array[String]]

Parameters:

Returns:

  • (Array[Array[String]]) 


106
107
108
109
110
111
112
 
# File 'lib/ibex/equiv.rb', line 106

def generated_samples(grammar, seed)
  Samples.new(
    grammar, seed: seed, max_tokens: @max_tokens, max_depth: [@max_tokens * 2, 16].max,
             max_expansions: [Samples::DEFAULT_MAX_EXPANSIONS, @sample_count * @max_tokens * 8].max,
             strategy: :coverage, path_length: 2
  ).generate(count: @sample_count)
end

#grammar_signature(grammar, map_left:) ⇒ Hash[Symbol, Object?]

RBS:

  • (IR::Grammar grammar, map_left: bool) -> Hash[Symbol, Object?]

Parameters:

Returns:

  • (Hash[Symbol, Object?]) 


232
233
234
235
236
237
238
239
 
# File 'lib/ibex/equiv.rb', line 232

def grammar_signature(grammar, map_left:)
  {
    starts: grammar.starts.map { |name| mapped_name(grammar, name, map_left: map_left) },
    recovery: recovery_signature(grammar, map_left: map_left),
    terminals: terminal_signatures(grammar),
    productions: production_signatures(grammar, map_left: map_left)
  }
end

#mapped_name(grammar, name, map_left:) ⇒ String

RBS:

  • (IR::Grammar grammar, String name, map_left: bool) -> String

Parameters:

  • grammar (IR::Grammar)
  • name (String)
  • map_left: (Boolean)

Returns:

  • (String) 


284
285
286
287
288
289
 
# File 'lib/ibex/equiv.rb', line 284

def mapped_name(grammar, name, map_left:)
  symbol = grammar.symbol(name)
  return name unless map_left && symbol&.nonterminal?

  @rule_map.fetch(name, name)
end

#node_signature(node) ⇒ tree_node_signature?

RBS:

  • (IR::node_annotation? node) -> tree_node_signature?

Parameters:

  • node (IR::node_annotation, nil)

Returns:

  • (tree_node_signature, nil) 


211
212
213
 
# File 'lib/ibex/equiv.rb', line 211

def node_signature(node)
  node && [node.fetch(:name), node.fetch(:fields)]
end

#product_key(left, right) ⇒ Array[Object?]

RBS:

  • (Machine::Configuration left, Machine::Configuration right) -> Array[Object?]

Parameters:

Returns:

  • (Array[Object?]) 


324
325
326
327
328
 
# File 'lib/ibex/equiv.rb', line 324

def product_key(left, right)
  key = [left.stack, left.status, left.actions, right.stack, right.status, right.actions]
  key.push(left.reductions, right.reductions) if tree_requested?
  key
end

#production_signature(grammar, production, map_left:) ⇒ production_signature

RBS:

  • (IR::Grammar grammar, IR::Production production, map_left: bool) -> production_signature

Parameters:

Returns:



265
266
267
268
269
270
271
272
273
274
275
 
# File 'lib/ibex/equiv.rb', line 265

def production_signature(grammar, production, map_left:)
  lhs = symbol_name(grammar, production.lhs)
  rhs = production.rhs.map { |id| symbol_name(grammar, id) }
  precedence = production.precedence_override
  precedence_name = symbol_name(grammar, precedence) if precedence
  [
    mapped_name(grammar, lhs, map_left: map_left),
    rhs.map { |name| mapped_name(grammar, name, map_left: map_left) },
    precedence_name && mapped_name(grammar, precedence_name, map_left: map_left)
  ]
end

#production_signatures(grammar, map_left:) ⇒ Array[production_signature]

RBS:

  • (IR::Grammar grammar, map_left: bool) -> Array[production_signature]

Parameters:

Returns:



260
261
262
 
# File 'lib/ibex/equiv.rb', line 260

def production_signatures(grammar, map_left:)
  grammar.productions.map { |production| production_signature(grammar, production, map_left: map_left) }
end

#raise_language_difference(tokens, left, right, method) ⇒ bot

RBS:

  • (Array[String] tokens, Symbol? left, Symbol? right, String method) -> bot

Parameters:

  • tokens (Array[String])
  • left (Symbol, nil)
  • right (Symbol, nil)
  • method (String)

Returns:

  • (bot) 


183
184
185
186
187
188
189
190
 
# File 'lib/ibex/equiv.rb', line 183

def raise_language_difference(tokens, left, right, method)
  raise Difference.new(
    ibex_report: "equiv", schema_version: 1, result: "difference",
    difference_kind: "language", method: method, witness: tokens, outcomes: { left: left, right: right },
    direction: left == :accepted ? "left_only" : "right_only",
    bounds: bounds, statement: CAVEAT
  )
end

#recovery_signature(grammar, map_left:) ⇒ Hash[Symbol, Object?]

RBS:

  • (IR::Grammar grammar, map_left: bool) -> Hash[Symbol, Object?]

Parameters:

Returns:

  • (Hash[Symbol, Object?]) 


242
243
244
245
246
247
248
249
 
# File 'lib/ibex/equiv.rb', line 242

def recovery_signature(grammar, map_left:)
  {
    sync_tokens: grammar.recovery.fetch(:sync_tokens),
    on_error_reduce: grammar.recovery.fetch(:on_error_reduce).map do |group|
      group.map { |name| mapped_name(grammar, name, map_left: map_left) }
    end
  }
end

#run ⇒ Hash[Symbol, Object?]

RBS:

  • () -> Hash[Symbol, Object?]

Returns:

  • (Hash[Symbol, Object?]) 


70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
 
# File 'lib/ibex/equiv.rb', line 70

def run
  verify_inputs!
  structural = structural_identity?
  tree_structural = tree_structural_identity?
  return successful_report(structural: true, samples: 0, configurations: 0) if structural && tree_structural

  samples = compare_samples
  configurations = search_product
  successful_report(structural: false, samples: samples, configurations: configurations)
rescue Machine::BudgetExceeded => e
  raise BudgetExceeded.new(
    result: "budget_exhausted", phase: "simulation", message: e.message,
    bounds: bounds, statement: CAVEAT
  )
rescue Ibex::Error => e
  raise if e.is_a?(Difference) || e.is_a?(BudgetExceeded)
  raise unless sample_budget_error?(e)

  raise BudgetExceeded.new(
    result: "budget_exhausted", phase: "sampling", message: e.message,
    bounds: bounds, statement: CAVEAT
  )
end

#sample_budget_error?(error) ⇒ Boolean

RBS:

  • (Ibex::Error error) -> bool

Parameters:

Returns:

  • (Boolean) 


368
369
370
 
# File 'lib/ibex/equiv.rb', line 368

def sample_budget_error?(error)
  error.message.match?(/(?:limit|maximum|budget).*(?:exceed|exhaust)|needs \d+ tokens/i)
end

#search_product ⇒ Integer

RBS:

  • () -> Integer

Returns:

  • (Integer) 


115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
 
# File 'lib/ibex/equiv.rb', line 115

def search_product # rubocop:disable Metrics/MethodLength -- BFS lifecycle remains visible as one bounded worklist.
  left_start = @left_machine.start
  right_start = @right_machine.start
  queue = [[left_start, right_start, []]] #: Array[[Machine::Configuration, Machine::Configuration, Array[String]]]
  seen = { product_key(left_start, right_start) => true }
  cursor = 0
  truncated = false
  alphabet = terminal_alphabet

  while cursor < queue.length
    left, right, tokens = queue.fetch(cursor)
    cursor += 1
    compare_configurations!(left, right, tokens)
    next if tokens.length >= @max_tokens || both_rejected?(left, right)

    alphabet.each do |token|
      next_left = @left_machine.push(left, token)
      next_right = @right_machine.push(right, token)
      key = product_key(next_left, next_right)
      next if seen[key]

      if queue.length >= @max_configurations
        truncated = true
        next
      end
      seen[key] = true
      queue << [next_left, next_right, tokens + [token]]
    end
  end
  if truncated
    raise BudgetExceeded.new(
      result: "budget_exhausted", phase: "product_bfs", checked_configurations: cursor,
      bounds: bounds, statement: CAVEAT
    )
  end

  cursor
end

#structural_identity? ⇒ Boolean

RBS:

  • () -> bool

Returns:

  • (Boolean) 


193
194
195
196
 
# File 'lib/ibex/equiv.rb', line 193

def structural_identity?
  @left.algorithm == @right.algorithm &&
    grammar_signature(@left.grammar, map_left: true) == grammar_signature(@right.grammar, map_left: false)
end

#successful_report(structural:, samples:, configurations:) ⇒ Object

RBS:

  • (structural: bool, samples: Integer, configurations: Integer) -> untyped

Parameters:

  • structural: (Boolean)
  • samples: (Integer)
  • configurations: (Integer)

Returns:

  • (Object) 


336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
 
# File 'lib/ibex/equiv.rb', line 336

def successful_report(structural:, samples:, configurations:)
  methods = if structural
              ["structural_comparison"]
            else
              %w[structural_comparison bidirectional_sampling bounded_product_bfs]
            end
  IR.deep_freeze(
    ibex_report: "equiv", schema_version: 1, result: "no_difference_within_bounds",
    structural_identity: structural,
    methods: methods,
    rule_map: @rule_map,
    tree: {
      requested: tree_requested?,
      result: tree_requested? ? "no_difference_within_bounds" : "not_checked"
    },
    checked: { samples: samples, product_configurations: configurations },
    bounds: bounds, statement: CAVEAT
  )
end

#symbol_name(grammar, id) ⇒ String

RBS:

  • (IR::Grammar grammar, Integer id) -> String

Parameters:

Returns:

  • (String) 


278
279
280
281
 
# File 'lib/ibex/equiv.rb', line 278

def symbol_name(grammar, id)
  symbol = grammar.symbol_by_id(id)
  symbol ? symbol.name : id.to_s
end

#terminal_alphabet ⇒ Array[String]

RBS:

  • () -> Array[String]

Returns:

  • (Array[String]) 


317
318
319
320
321
 
# File 'lib/ibex/equiv.rb', line 317

def terminal_alphabet
  [@left, @right].flat_map do |automaton|
    automaton.grammar.terminals.reject(&:reserved).map(&:name)
  end.uniq.sort
end

#terminal_signatures(grammar) ⇒ Array[terminal_signature]

RBS:

  • (IR::Grammar grammar) -> Array[terminal_signature]

Parameters:

Returns:

  • (Array[terminal_signature]) 


252
253
254
255
256
257
 
# File 'lib/ibex/equiv.rb', line 252

def terminal_signatures(grammar)
  grammar.terminals.map do |symbol|
    precedence = symbol.precedence
    [symbol.name, precedence && [precedence.fetch(:associativity), precedence.fetch(:level)]]
  end
end

#tree_grammar_signature(grammar) ⇒ Array[tree_node_signature]

RBS:

  • (IR::Grammar grammar) -> Array[tree_node_signature]

Parameters:

Returns:

  • (Array[tree_node_signature]) 


206
207
208
 
# File 'lib/ibex/equiv.rb', line 206

def tree_grammar_signature(grammar)
  grammar.productions.filter_map { |production| node_signature(production.node) }
end

#tree_requested? ⇒ Boolean

RBS:

  • () -> bool

Returns:

  • (Boolean) 


357
 
# File 'lib/ibex/equiv.rb', line 357

def tree_requested? = !@rule_map.empty?

#tree_structural_identity? ⇒ Boolean

RBS:

  • () -> bool

Returns:

  • (Boolean) 


199
200
201
202
203
 
# File 'lib/ibex/equiv.rb', line 199

def tree_structural_identity?
  return true unless tree_requested?

  tree_grammar_signature(@left.grammar) == tree_grammar_signature(@right.grammar)
end

#tree_trace(automaton, configuration, map_left:) ⇒ Array[tree_trace_entry]

RBS:

  • (IR::Automaton automaton, Machine::Configuration configuration, map_left: bool) -> Array[tree_trace_entry]

Parameters:

Returns:

  • (Array[tree_trace_entry]) 


216
217
218
219
220
221
222
223
224
225
226
227
228
229
 
# File 'lib/ibex/equiv.rb', line 216

def tree_trace(automaton, configuration, map_left:)
  configuration.reductions.map do |production_id|
    production = automaton.grammar.productions.fetch(production_id)
    lhs = symbol_name(automaton.grammar, production.lhs)
    [
      mapped_name(automaton.grammar, lhs, map_left: map_left),
      production.rhs.map do |id|
        mapped_name(automaton.grammar, symbol_name(automaton.grammar, id),
                    map_left: map_left)
      end,
      node_signature(production.node)
    ]
  end
end

#validate_rule_map! ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



292
293
294
295
296
297
298
299
300
301
302
 
# File 'lib/ibex/equiv.rb', line 292

def validate_rule_map!
  left_names = @left.grammar.nonterminals.map(&:name)
  right_names = @right.grammar.nonterminals.map(&:name)
  unknown_left = @rule_map.keys - left_names
  unknown_right = @rule_map.values - right_names
  raise ArgumentError, "unknown left rules: #{unknown_left.join(', ')}" unless unknown_left.empty?
  raise ArgumentError, "unknown right rules: #{unknown_right.join(', ')}" unless unknown_right.empty?
  return if @rule_map.values.uniq.length == @rule_map.length

  raise ArgumentError, "rule map must be one-to-one"
end

#verify_inputs! ⇒ void

This method returns an undefined value.

RBS:

  • () -> void



305
306
307
308
309
310
311
312
313
314
 
# File 'lib/ibex/equiv.rb', line 305

def verify_inputs!
  { left: @left, right: @right }.each do |side, automaton|
    result = Verify::Verifier.new(automaton).verify
    next if result.valid?

    raise Ibex::Error,
          "(equiv):1:1: #{side} automaton failed independent verification: " \
          "#{result.violations.first&.message}"
  end
end