Class: Ibex::Fix

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

Overview

Bounded conflict-repair candidate generation and safety evaluation. rubocop:disable Metrics/ClassLength -- candidate generation and its three safety gates share one target identity.

Defined Under Namespace

Classes: BudgetExceeded

Constant Summary collapse

SCHEMA_VERSION =

RBS:

  • type candidate = { category: String, description: String, source: String?, algorithm: Symbol }

Returns:

  • (Integer) 
3
CATEGORIES =

Signature:

  • Integer

Returns:

  • (Array[String]) 
%w[
  precedence_declaration precedence_override algorithm_change
  mechanical_rewrite
].freeze
ADVICE_CATEGORIES =

Signature:

  • Array[String]

Returns:

  • (Array[String]) 
%w[expectation_declaration recovery_quality].freeze
ADVICE_STATEMENT =

Signature:

  • Array[String]

Returns:

  • (String) 
"Advice does not eliminate the selected conflict and is not a verified repair."

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(source, file:, grammar:, automaton:, algorithm:, mode:, state: nil, conflict_index: nil, max_candidates: 32, max_builds: 32, equiv_max_tokens: 8, equiv_max_configurations: 50_000, equiv_samples: 100, verify_max_states: 100_000, verify_max_items: 1_000_000, messages: nil, message_file: nil) ⇒ Fix

rubocop:disable Metrics/ParameterLists

RBS:

  • (String source, file: String, grammar: IR::Grammar, automaton: IR::Automaton, algorithm: Symbol, mode: Symbol, ?state: Integer?, ?conflict_index: Integer?, ?max_candidates: Integer, ?max_builds: Integer, ?equiv_max_tokens: Integer, ?equiv_max_configurations: Integer, ?equiv_samples: Integer, ?verify_max_states: Integer, ?verify_max_items: Integer, ?messages: ErrorMessages::Document?, ?message_file: String?) -> void

Parameters:

  • source (String)
  • file: (String)
  • grammar: (IR::Grammar)
  • automaton: (IR::Automaton)
  • algorithm: (Symbol)
  • mode: (Symbol)
  • state: (Integer, nil) (defaults to: nil)
  • conflict_index: (Integer, nil) (defaults to: nil)
  • max_candidates: (Integer) (defaults to: 32)
  • max_builds: (Integer) (defaults to: 32)
  • equiv_max_tokens: (Integer) (defaults to: 8)
  • equiv_max_configurations: (Integer) (defaults to: 50_000)
  • equiv_samples: (Integer) (defaults to: 100)
  • verify_max_states: (Integer) (defaults to: 100_000)
  • verify_max_items: (Integer) (defaults to: 1_000_000)
  • messages: (ErrorMessages::Document, nil) (defaults to: nil)
  • message_file: (String, nil) (defaults to: nil) 


41
42
43
44
45
46
47
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
75
 
# File 'lib/ibex/fix.rb', line 41

def initialize(source, file:, grammar:, automaton:, algorithm:, mode:, state: nil, conflict_index: nil,
               max_candidates: 32, max_builds: 32, equiv_max_tokens: 8,
               equiv_max_configurations: 50_000, equiv_samples: 100,
               verify_max_states: 100_000, verify_max_items: 1_000_000,
               messages: nil, message_file: nil)
  { max_candidates: max_candidates, max_builds: max_builds, equiv_max_tokens: equiv_max_tokens,
    equiv_max_configurations: equiv_max_configurations, equiv_samples: equiv_samples,
    verify_max_states: verify_max_states, verify_max_items: verify_max_items }.each do |name, value|
    raise ArgumentError, "#{name} must be positive" unless value.positive?
  end

  @source = source
  if source.match?(/^# #{Regexp.escape(BisonImport::STRUCTURAL_STATUS_MARKER)}: incomplete$/)
    raise Ibex::Error,
          "(fix):1:1: cannot propose repairs for a structurally incomplete Bison import"
  end
  @file = file
  @grammar = grammar
  @automaton = automaton
  @algorithm = algorithm
  @mode = mode
  @requested_state = state
  @requested_conflict_index = conflict_index
  @max_candidates = max_candidates
  @max_builds = max_builds
  @equiv_max_tokens = equiv_max_tokens
  @equiv_max_configurations = equiv_max_configurations
  @equiv_samples = equiv_samples
  @verify_max_states = verify_max_states
  @verify_max_items = verify_max_items
  @messages = messages
  @message_file = message_file
  @sources = {}
  @builds = 0
end

Instance Attribute Details

#sources ⇒ Hash[String, String] (readonly)

Signature:

  • Hash[String, String]

Returns:

  • (Hash[String, String]) 


33
34
35
 
# File 'lib/ibex/fix.rb', line 33

def sources
  @sources
end

Instance Method Details

#active_conflict?(conflict) ⇒ Boolean

RBS:

  • (IR::conflict conflict) -> bool

Parameters:

  • conflict (IR::conflict)

Returns:

  • (Boolean) 


429
430
431
432
433
 
# File 'lib/ibex/fix.rb', line 429

def active_conflict?(conflict)
  return true if conflict.fetch(:type).to_sym == :reduce_reduce

  conflict.fetch(:resolution).fetch(:by).to_sym == :default_shift
end

#active_conflicts(automaton) ⇒ Array[[ IR::AutomatonState, IR::conflict ]]

RBS:

  • (IR::Automaton automaton) -> Array[[IR::AutomatonState, IR::conflict]]

Parameters:

Returns:



422
423
424
425
426
 
# File 'lib/ibex/fix.rb', line 422

def active_conflicts(automaton)
  automaton.states.flat_map do |state|
    state.conflicts.filter_map { |conflict| [state, conflict] if active_conflict?(conflict) }
  end
end

#advice_space(conflict) ⇒ Array[Hash[Symbol, Object?]]

RBS:

  • (IR::conflict conflict) -> Array[Hash[Symbol, Object?]]

Parameters:

  • conflict (IR::conflict)

Returns:

  • (Array[Hash[Symbol, Object?]]) 


143
144
145
146
147
148
149
150
151
152
153
 
# File 'lib/ibex/fix.rb', line 143

def advice_space(conflict)
  [expectation_candidate(conflict), recovery_candidate(conflict)].compact.map do |candidate|
    source = candidate[:source]
    diff = source && source != @source ? unified_diff(@source, source) : nil
    {
      category: candidate.fetch(:category), description: candidate.fetch(:description),
      source_change: !diff.nil?, unified_diff: diff,
      statement: ADVICE_STATEMENT
    }
  end
end

#algorithm_candidates ⇒ Array[candidate]

RBS:

  • () -> Array[candidate]

Returns:



191
192
193
194
195
 
# File 'lib/ibex/fix.rb', line 191

def algorithm_candidates
  %i[ielr lr1].reject { |algorithm| algorithm == @algorithm }.map do |algorithm|
    candidate("algorithm_change", "construct with #{algorithm}", algorithm: algorithm)
  end
end

#append_to_line(line_number, suffix) ⇒ String

RBS:

  • (Integer line_number, String suffix) -> String

Parameters:

  • line_number (Integer)
  • suffix (String)

Returns:

  • (String) 


497
498
499
500
501
502
503
504
505
506
 
# File 'lib/ibex/fix.rb', line 497

def append_to_line(line_number, suffix)
  source = @source #: String
  lines = source.lines
  line = lines.fetch(line_number - 1)
  ending = line.end_with?("\n") ? "\n" : ""
  lines[line_number - 1] = "#{line.delete_suffix("\n")}#{suffix}#{ending}"
  lines.join
rescue IndexError
  raise Ibex::Error, "(fix):1:1: production source line is outside the root file"
end

#bounds ⇒ Hash[Symbol, Integer]

RBS:

  • () -> Hash[Symbol, Integer]

Returns:

  • (Hash[Symbol, Integer]) 


547
548
549
550
551
552
553
554
 
# File 'lib/ibex/fix.rb', line 547

def bounds
  {
    max_candidates: @max_candidates, max_builds: @max_builds,
    equiv_samples: @equiv_samples, equiv_max_tokens: @equiv_max_tokens,
    equiv_max_configurations: @equiv_max_configurations,
    verify_max_states: @verify_max_states, verify_max_items: @verify_max_items
  }
end

#build_candidate(candidate) ⇒ IR::Automaton

RBS:

  • (candidate candidate) -> IR::Automaton

Parameters:

Returns:



320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
 
# File 'lib/ibex/fix.rb', line 320

def build_candidate(candidate)
  builds = @builds #: Integer
  max_builds = @max_builds #: Integer
  raise BudgetExceeded, { result: "budget_exhausted", phase: "builds", bounds: bounds } if builds >= max_builds

  @builds = builds + 1
  source = candidate[:source]
  grammar = if source
              ast = Frontend::Parser.new(source, file: @file, mode: @mode).parse
              Normalizer.new(ast, mode: @mode).normalize
            else
              @grammar
            end
  grammar = Configuration::AnalysisGrammar.for_algorithm(grammar, candidate.fetch(:algorithm))
  LALR::Builder.new(grammar, algorithm: candidate.fetch(:algorithm)).build
end

#candidate(category, description, source: nil, algorithm: nil) ⇒ candidate

RBS:

  • (String category, String description, ?source: String?, ?algorithm: Symbol?) -> candidate

Parameters:

  • category (String)
  • description (String)
  • source: (String, nil) (defaults to: nil)
  • algorithm: (Symbol, nil) (defaults to: nil)

Returns:



254
255
256
 
# File 'lib/ibex/fix.rb', line 254

def candidate(category, description, source: nil, algorithm: nil)
  { category: category, description: description, source: source, algorithm: algorithm || @algorithm }
end

#candidate_space(conflict) ⇒ Array[candidate]

RBS:

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

Parameters:

  • conflict (IR::conflict)

Returns:



132
133
134
135
136
137
138
139
140
 
# File 'lib/ibex/fix.rb', line 132

def candidate_space(conflict)
  candidates = precedence_declaration_candidates(conflict)
  override = precedence_override_candidate(conflict)
  candidates << override if override
  candidates.concat(algorithm_candidates)
  rewrite = inline_candidate(conflict)
  candidates << rewrite if rewrite
  candidates
end

#conflict_counts(automaton) ⇒ Hash[String, Integer]

RBS:

  • (IR::Automaton automaton) -> Hash[String, Integer]

Parameters:

Returns:

  • (Hash[String, Integer]) 


445
446
447
448
449
 
# File 'lib/ibex/fix.rb', line 445

def conflict_counts(automaton)
  active_conflicts(automaton).each_with_object(Hash.new(0)) do |(_state, conflict), counts|
    counts[conflict_fingerprint(automaton.grammar, conflict)] += 1
  end
end

#conflict_fingerprint(grammar, conflict) ⇒ String

RBS:

  • (IR::Grammar grammar, IR::conflict conflict) -> String

Parameters:

Returns:

  • (String) 


452
453
454
455
456
457
458
459
460
461
462
 
# File 'lib/ibex/fix.rb', line 452

def conflict_fingerprint(grammar, conflict)
  if conflict.fetch(:type).to_sym == :shift_reduce
    shift_reduce = conflict #: IR::shift_reduce_conflict
    "shift_reduce:#{shift_reduce.fetch(:symbol)}:" \
      "#{production_shape(grammar, shift_reduce.fetch(:reduce))}"
  else
    reduce_reduce = conflict #: IR::reduce_reduce_conflict
    shapes = reduce_reduce.fetch(:reductions).map { |id| production_shape(grammar, id) }.sort
    "reduce_reduce:#{reduce_reduce.fetch(:symbol)}:#{shapes.join('|')}"
  end
end

#conflict_safety_failure(candidate, target) ⇒ Hash[Symbol, String]?

RBS:

  • (IR::Automaton candidate, IR::conflict target) -> Hash[Symbol, String]?

Parameters:

Returns:

  • (Hash[Symbol, String], nil) 


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

def conflict_safety_failure(candidate, target)
  grammar = @grammar #: IR::Grammar
  automaton = @automaton #: IR::Automaton
  fingerprint = conflict_fingerprint(grammar, target)
  active = active_conflicts(candidate)
  original_active = active_conflicts(automaton)
  return { status: "rejected", reason: "target_conflict_remains" } if
    active.any? { |_state, conflict| conflict_fingerprint(candidate.grammar, conflict) == fingerprint }
  return { status: "rejected", reason: "conflict_count_did_not_decrease" } unless
    active.length < original_active.length

  { status: "rejected", reason: "other_conflicts_increased" } if
    increased_other_conflict?(candidate, fingerprint)
end

#evaluate_candidate(candidate, target) ⇒ Hash[Symbol, Object?]

RBS:

  • (candidate candidate, IR::conflict target) -> Hash[Symbol, Object?]

Parameters:

  • candidate (candidate)
  • target (IR::conflict)

Returns:

  • (Hash[Symbol, Object?]) 


259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
 
# File 'lib/ibex/fix.rb', line 259

def evaluate_candidate(candidate, target)
  candidate_automaton = build_candidate(candidate)
  failure = conflict_safety_failure(candidate_automaton, target)
  return failure if failure

  failure = verification_safety_failure(candidate_automaton)
  return failure if failure

  equivalence = Equiv.new(
    @automaton, candidate_automaton,
    sample_count: @equiv_samples, max_tokens: @equiv_max_tokens,
    max_configurations: @equiv_max_configurations,
    rule_map: identity_rule_map(candidate_automaton.grammar)
  ).run
  {
    status: "safe", automaton: candidate_automaton, equivalence: equivalence,
    removed_conflicts: active_conflicts(@automaton).length - active_conflicts(candidate_automaton).length
  }
rescue Equiv::Difference
  { status: "rejected", reason: "bounded_language_or_tree_difference" }
rescue Equiv::BudgetExceeded
  { status: "rejected", reason: "equivalence_budget_exhausted" }
rescue Verify::BudgetExceeded
  { status: "rejected", reason: "verification_budget_exhausted" }
rescue BudgetExceeded
  raise
rescue Ibex::Error, ArgumentError => e
  { status: "rejected", reason: "candidate_build_failed", message: e.message }
end

#expectation_candidate(conflict) ⇒ candidate

RBS:

  • (IR::conflict conflict) -> candidate

Parameters:

  • conflict (IR::conflict)

Returns:



220
221
222
223
224
225
226
227
228
229
230
231
 
# File 'lib/ibex/fix.rb', line 220

def expectation_candidate(conflict)
  automaton = @automaton #: IR::Automaton
  directive = if conflict.fetch(:type).to_sym == :reduce_reduce
                "%expect-rr #{automaton.conflict_summary.fetch(:rr)}\n"
              else
                "expect #{automaton.conflict_summary.fetch(:sr)}\n"
              end
  candidate(
    "expectation_declaration", "acknowledge the current conflict count",
    source: replace_or_insert_expectation(directive)
  )
end

#identity_rule_map(candidate_grammar) ⇒ Hash[String, String]

RBS:

  • (IR::Grammar candidate_grammar) -> Hash[String, String]

Parameters:

Returns:

  • (Hash[String, String]) 


473
474
475
476
477
478
 
# File 'lib/ibex/fix.rb', line 473

def identity_rule_map(candidate_grammar)
  grammar = @grammar #: IR::Grammar
  left = grammar.nonterminals.map(&:name)
  right = candidate_grammar.nonterminals.map(&:name)
  (left & right).to_h { |name| [name, name] }
end

#increased_other_conflict?(candidate, target_fingerprint) ⇒ Boolean

RBS:

  • (IR::Automaton candidate, String target_fingerprint) -> bool

Parameters:

Returns:

  • (Boolean) 


436
437
438
439
440
441
442
 
# File 'lib/ibex/fix.rb', line 436

def increased_other_conflict?(candidate, target_fingerprint)
  before = conflict_counts(@automaton)
  after = conflict_counts(candidate)
  after.any? do |fingerprint, count|
    fingerprint != target_fingerprint && count > before.fetch(fingerprint, 0)
  end
end

#inline_candidate(conflict) ⇒ candidate?

RBS:

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

Parameters:

  • conflict (IR::conflict)

Returns:



198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
 
# File 'lib/ibex/fix.rb', line 198

def inline_candidate(conflict)
  production_id = if conflict.fetch(:type).to_sym == :shift_reduce
                    shift_reduce = conflict #: IR::shift_reduce_conflict
                    shift_reduce.fetch(:reduce)
                  else
                    reduce_reduce = conflict #: IR::reduce_reduce_conflict
                    reduce_reduce.fetch(:reductions).first
                  end
  grammar = @grammar #: IR::Grammar
  source = @source #: String
  production = grammar.productions.fetch(production_id)
  lhs = grammar.symbol_by_id(production.lhs)&.name
  return unless lhs && !grammar.starts.include?(lhs)

  pattern = /^(\s*)#{Regexp.escape(lhs)}\s*:/
  return unless source.match?(pattern)

  edited = update_expectation(source.sub(pattern, "\\1%inline #{lhs}:"), conflict)
  candidate("mechanical_rewrite", "inline nonterminal #{lhs}", source: edited)
end

#insert_before_rule(insertion) ⇒ String

RBS:

  • (String insertion) -> String

Parameters:

  • insertion (String)

Returns:

  • (String) 


481
482
483
 
# File 'lib/ibex/fix.rb', line 481

def insert_before_rule(insertion)
  insert_before_rule_in(@source, insertion)
end

#insert_before_rule_in(source, insertion) ⇒ String

RBS:

  • (String source, String insertion) -> String

Parameters:

  • source (String)
  • insertion (String)

Returns:

  • (String) 


486
487
488
489
490
491
492
493
494
 
# File 'lib/ibex/fix.rb', line 486

def insert_before_rule_in(source, insertion)
  match = source.match(/^rule\b/)
  raise Ibex::Error, "(fix):1:1: source has no rule section" unless match

  offset = match.begin(0)
  raise Ibex::Error, "(fix):1:1: rule section has no source offset" unless offset

  source.dup.insert(offset, insertion)
end

#message_catalog_impact(candidate) ⇒ Hash[Symbol, Object?]

RBS:

  • (IR::Automaton candidate) -> Hash[Symbol, Object?]

Parameters:

Returns:

  • (Hash[Symbol, Object?]) 


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

def message_catalog_impact(candidate)
  unless @messages
    empty = [] #: Array[String]
    return { status: "not_configured", moved: empty, uncovered: empty, unreachable: empty }
  end

  file = @message_file || "(messages)"
  automaton = @automaton #: IR::Automaton
  baseline = ErrorMessages.update(automaton, existing: @messages)
  changed = ErrorMessages.update(candidate, existing: @messages)
  {
    status: "evaluated", file: file,
    moved: changed.moved - baseline.moved,
    uncovered: changed.uncovered - baseline.uncovered,
    unreachable: changed.unreachable - baseline.unreachable
  }
end

#precedence_declaration_candidates(conflict) ⇒ Array[candidate]

RBS:

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

Parameters:

  • conflict (IR::conflict)

Returns:



156
157
158
159
160
161
162
163
164
165
166
167
168
 
# File 'lib/ibex/fix.rb', line 156

def precedence_declaration_candidates(conflict)
  return [] unless conflict.fetch(:type).to_sym == :shift_reduce

  %w[left right nonassoc %precedence].map do |associativity|
    block = "preclow\n  #{associativity} #{conflict.fetch(:symbol)}\nprechigh\n"
    edited = update_expectation(insert_before_rule(block), conflict)
    candidate(
      "precedence_declaration",
      "declare #{associativity} precedence for #{conflict.fetch(:symbol)}",
      source: edited
    )
  end
end

#precedence_override_candidate(conflict) ⇒ candidate?

RBS:

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

Parameters:

  • conflict (IR::conflict)

Returns:



171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
 
# File 'lib/ibex/fix.rb', line 171

def precedence_override_candidate(conflict)
  return unless conflict.fetch(:type).to_sym == :shift_reduce

  value = conflict #: IR::shift_reduce_conflict
  grammar = @grammar #: IR::Grammar
  production = grammar.productions.fetch(value.fetch(:reduce))
  return if production.node

  line = production.origin.dig(:loc, :line)
  return unless line

  edited = update_expectation(append_to_line(line, " = #{value.fetch(:symbol)}"), conflict)
  candidate(
    "precedence_override",
    "override production #{production.id} precedence with #{value.fetch(:symbol)}",
    source: edited
  )
end

#production_shape(grammar, id) ⇒ String

RBS:

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

Parameters:

Returns:

  • (String) 


465
466
467
468
469
470
 
# File 'lib/ibex/fix.rb', line 465

def production_shape(grammar, id)
  production = grammar.productions.fetch(id)
  lhs = grammar.symbol_by_id(production.lhs)&.name || production.lhs.to_s
  rhs = production.rhs.map { |symbol| grammar.symbol_by_id(symbol)&.name || symbol.to_s }
  "#{lhs}->#{rhs.join(' ')}"
end

#proposal(candidate, outcome, conflict, number) ⇒ Hash[Symbol, Object?]

RBS:

  • (candidate candidate, Hash[Symbol, Object?] outcome, IR::conflict conflict, Integer number) -> Hash[Symbol, Object?]

Parameters:

  • candidate (candidate)
  • outcome (Hash[Symbol, Object?])
  • conflict (IR::conflict)
  • number (Integer)

Returns:

  • (Hash[Symbol, Object?]) 


339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
 
# File 'lib/ibex/fix.rb', line 339

def proposal(candidate, outcome, conflict, number)
  id = format("FX%03d", number)
  source = candidate[:source]
  @sources[id] = source if source
  candidate_automaton = outcome.fetch(:automaton) #: IR::Automaton
  automaton = @automaton #: IR::Automaton
  grammar = @grammar #: IR::Grammar
  {
    id: id, category: candidate.fetch(:category), description: candidate.fetch(:description),
    algorithm: candidate.fetch(:algorithm), applyable: !source.nil?,
    unified_diff: source ? unified_diff(@source, source) : nil,
    eliminates: [conflict_fingerprint(grammar, conflict)],
    equivalence: outcome.fetch(:equivalence),
    side_effects: {
      states: {
        before: automaton.states.length, after: candidate_automaton.states.length,
        delta: candidate_automaton.states.length - automaton.states.length
      },
      removed_conflicts: outcome.fetch(:removed_conflicts),
      message_catalog: message_catalog_impact(candidate_automaton)
    }
  }
end

#recovery_candidate(conflict) ⇒ candidate?

RBS:

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

Parameters:

  • conflict (IR::conflict)

Returns:



234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
 
# File 'lib/ibex/fix.rb', line 234

def recovery_candidate(conflict)
  production_id = if conflict.fetch(:type).to_sym == :shift_reduce
                    shift_reduce = conflict #: IR::shift_reduce_conflict
                    shift_reduce.fetch(:reduce)
                  else
                    reduce_reduce = conflict #: IR::reduce_reduce_conflict
                    reduce_reduce.fetch(:reductions).first
                  end
  grammar = @grammar #: IR::Grammar
  production = grammar.productions.fetch(production_id)
  lhs = grammar.symbol_by_id(production.lhs)&.name
  return unless lhs

  candidate(
    "recovery_quality", "prefer #{lhs} during error recovery",
    source: insert_before_rule("%on_error_reduce #{lhs}\n")
  )
end

#rejection(candidate, outcome) ⇒ Hash[Symbol, Object?]

RBS:

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

Parameters:

  • candidate (candidate)
  • outcome (Hash[Symbol, Object?])

Returns:

  • (Hash[Symbol, Object?]) 


383
384
385
386
387
388
 
# File 'lib/ibex/fix.rb', line 383

def rejection(candidate, outcome)
  {
    category: candidate.fetch(:category), description: candidate.fetch(:description),
    reason: outcome.fetch(:reason), message: outcome[:message]
  }
end

#replace_or_insert_expectation(directive) ⇒ String

RBS:

  • (String directive) -> String

Parameters:

  • directive (String)

Returns:

  • (String) 


509
510
511
512
513
514
515
 
# File 'lib/ibex/fix.rb', line 509

def replace_or_insert_expectation(directive)
  pattern = directive.start_with?("%expect-rr") ? /^%expect-rr\s+\d+\s*$/ : /^expect\s+\d+\s*$/
  source = @source #: String
  return source.sub(pattern, directive.chomp) if source.match?(pattern)

  insert_before_rule(directive)
end

#report_for(state, index, conflict, candidates, proposals, rejections, advice) ⇒ Hash[Symbol, Object?]

RBS:

  • (IR::AutomatonState state, Integer index, IR::conflict conflict, Array[candidate] candidates, Array[Hash[Symbol, Object?]] proposals, Array[Hash[Symbol, Object?]] rejections, Array[Hash[Symbol, Object?]] advice) -> Hash[Symbol, Object?]

Parameters:

  • state (IR::AutomatonState)
  • index (Integer)
  • conflict (IR::conflict)
  • candidates (Array[candidate])
  • proposals (Array[Hash[Symbol, Object?]])
  • rejections (Array[Hash[Symbol, Object?]])
  • advice (Array[Hash[Symbol, Object?]])

Returns:

  • (Hash[Symbol, Object?]) 


393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
 
# File 'lib/ibex/fix.rb', line 393

def report_for(state, index, conflict, candidates, proposals, rejections, advice)
  inventory = CATEGORIES.to_h do |category|
    values = candidates.select { |candidate| candidate.fetch(:category) == category }
    rejected = rejections.count do |entry|
      record = entry #: { category: String }
      record.fetch(:category) == category
    end
    [category, { enumerated: values.length, rejected: rejected,
                 safe: proposals.count do |entry|
                   record = entry #: { category: String }
                   record.fetch(:category) == category
                 end }]
  end
  {
    ibex_report: "fix", schema_version: SCHEMA_VERSION,
    result: proposals.empty? ? "no_safe_proposal" : "proposals_found",
    target: {
      id: "state-#{state.id}-conflict-#{index}", state: state.id, index: index,
      type: conflict.fetch(:type), symbol: conflict.fetch(:symbol),
      fingerprint: conflict_fingerprint(@grammar, conflict)
    },
    candidate_space: inventory, advice: advice,
    proposals: proposals, rejections: rejections,
    bounds: bounds,
    statement: Equiv::CAVEAT
  }
end

#run ⇒ Hash[Symbol, Object?]

RBS:

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

Returns:

  • (Hash[Symbol, Object?]) 


79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
 
# File 'lib/ibex/fix.rb', line 79

def run
  state, index, conflict = select_target
  candidates = candidate_space(conflict)
  advice = advice_space(conflict)
  if candidates.length > @max_candidates
    details = {
      result: "budget_exhausted", phase: "candidate_enumeration",
      bounds: bounds, enumerated_candidates: candidates.length
    }
    raise BudgetExceeded, details
  end

  proposals = [] #: Array[Hash[Symbol, Object?]]
  rejections = [] #: Array[Hash[Symbol, Object?]]
  incomplete = false
  candidates.each do |candidate|
    outcome = evaluate_candidate(candidate, conflict)
    outcome_status = outcome.fetch(:status) #: String
    if outcome_status == "safe"
      proposals << proposal(candidate, outcome, conflict, proposals.length + 1)
    else
      outcome_reason = outcome.fetch(:reason) #: String
      incomplete ||= %w[equivalence_budget_exhausted verification_budget_exhausted]
                     .include?(outcome_reason)
      rejections << rejection(candidate, outcome)
    end
  end
  report = report_for(state, index, conflict, candidates, proposals, rejections, advice)
  raise BudgetExceeded, report.merge(result: "budget_exhausted", phase: "candidate_evaluation") if incomplete

  report
end

#select_target ⇒ [ IR::AutomatonState, Integer, IR::conflict ]

RBS:

  • () -> [IR::AutomatonState, Integer, IR::conflict]

Returns:



115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
 
# File 'lib/ibex/fix.rb', line 115

def select_target
  automaton = @automaton #: IR::Automaton
  states = @requested_state ? [automaton.states.fetch(@requested_state)] : automaton.states
  states.each do |state|
    state.conflicts.each_with_index do |conflict, index|
      next if @requested_conflict_index && index != @requested_conflict_index
      next unless active_conflict?(conflict)

      return [state, index, conflict]
    end
  end
  raise Ibex::Error, "(fix):1:1: no unresolved conflict matches the requested target"
rescue IndexError
  raise Ibex::Error, "(fix):1:1: requested state does not exist"
end

#unified_diff(before, after) ⇒ String

RBS:

  • (String before, String after) -> String

Parameters:

  • before (String)
  • after (String)

Returns:

  • (String) 


535
536
537
538
539
540
541
542
543
544
 
# File 'lib/ibex/fix.rb', line 535

def unified_diff(before, after)
  before_lines = before.lines
  after_lines = after.lines
  [
    "--- #{@file}", "+++ #{@file}",
    "@@ -1,#{before_lines.length} +1,#{after_lines.length} @@",
    *before_lines.map { |line| "-#{line.delete_suffix("\n")}" },
    *after_lines.map { |line| "+#{line.delete_suffix("\n")}" }
  ].join("\n") << "\n"
end

#update_expectation(source, conflict) ⇒ String

RBS:

  • (String source, IR::conflict conflict) -> String

Parameters:

  • source (String)
  • conflict (IR::conflict)

Returns:

  • (String) 


518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
 
# File 'lib/ibex/fix.rb', line 518

def update_expectation(source, conflict)
  automaton = @automaton #: IR::Automaton
  if conflict.fetch(:type).to_sym == :reduce_reduce
    current = automaton.conflict_summary.fetch(:rr)
    directive = "%expect-rr #{[current - 1, 0].max}"
    pattern = /^%expect-rr\s+\d+\s*$/
  else
    current = automaton.conflict_summary.fetch(:sr)
    directive = "expect #{[current - 1, 0].max}"
    pattern = /^expect\s+\d+\s*$/
  end
  return source.sub(pattern, directive) if source.match?(pattern)

  insert_before_rule_in(source, "#{directive}\n")
end

#verification_safety_failure(candidate) ⇒ Hash[Symbol, String]?

RBS:

  • (IR::Automaton candidate) -> Hash[Symbol, String]?

Parameters:

Returns:

  • (Hash[Symbol, String], nil) 


306
307
308
309
310
311
312
313
314
315
316
317
 
# File 'lib/ibex/fix.rb', line 306

def verification_safety_failure(candidate)
  verification = Verify::Verifier.new(
    candidate, max_states: @verify_max_states, max_items: @verify_max_items
  ).verify
  return { status: "rejected", reason: "candidate_failed_verification" } unless verification.valid?
  return { status: "rejected", reason: "conflict_expectation_mismatch" } unless
    candidate.conflict_summary.fetch(:expectation_met)
  return unless candidate.conflict_summary.key?(:rr_expectation_met) &&
                !candidate.conflict_summary.fetch(:rr_expectation_met)

  { status: "rejected", reason: "conflict_expectation_mismatch" }
end