Module: Ibex::CLIVerify

Defined in:
lib/ibex/cli/verify.rb,
sig/ibex/cli/verify.rbs

Overview

CLI entry point for bounded, independent Automaton IR verification.

Instance Method Summary collapse

Instance Method Details

#load_verify_automaton(path) ⇒ IR::Automaton

RBS:

  • (String path) -> IR::Automaton

Parameters:

  • path (String)

Returns:



80
81
82
83
84
85
 
# File 'lib/ibex/cli/verify.rb', line 80

def load_verify_automaton(path)
  value = IR::Validator.validate(File.binread(path))
  return value if value.is_a?(IR::Automaton)

  raise Ibex::Error, "#{path}:1:1: verify requires Automaton IR"
end

#positive_verify_budget(value, name) ⇒ Integer

RBS:

  • (Integer value, String name) -> Integer

Parameters:

  • value (Integer)
  • name (String)

Returns:

  • (Integer) 


110
111
112
113
114
 
# File 'lib/ibex/cli/verify.rb', line 110

def positive_verify_budget(value, name)
  return value if value.positive?

  raise OptionParser::InvalidArgument, "--#{name} must be positive"
end

#run_verify_command(arguments) ⇒ Integer

RBS:

  • (Array[String] arguments) -> Integer

Parameters:

  • arguments (Array[String])

Returns:

  • (Integer) 


26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
 
# File 'lib/ibex/cli/verify.rb', line 26

def run_verify_command(arguments)
  settings = verify_options(arguments)
  if settings[:help]
    @stdout.puts(settings.fetch(:help))
    return 0
  end
  operands = settings.fetch(:paths)
  raise Ibex::Error, "(verify):1:1: verify requires exactly one Automaton IR file" unless operands.length == 1

  automaton = load_verify_automaton(operands.fetch(0))
  verify_supplied_grammar!(automaton, settings[:grammar]) if settings[:grammar]
  result = Verify::Verifier.new(
    automaton,
    strict: settings.fetch(:strict),
    max_states: settings.fetch(:max_states),
    max_items: settings.fetch(:max_items)
  ).verify
  write_verify_result(result, settings.fetch(:format))
  result.valid? ? 0 : 1
rescue Verify::BudgetExceeded => e
  violations = [] #: Array[Verify::Violation]
  report = {
    ibex_report: "verify", schema_version: 1, result: "budget_exhausted",
    strict: settings&.fetch(:strict, false), bounds: e.bounds, violations: violations
  }
  @stdout.puts(JSON.pretty_generate(report))
  2
end

#verify_options(arguments) ⇒ verify_options

RBS:

  • (Array[String] arguments) -> verify_options

Parameters:

  • arguments (Array[String])

Returns:



56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
 
# File 'lib/ibex/cli/verify.rb', line 56

def verify_options(arguments)
  settings = {
    paths: [], strict: false, max_states: 100_000, max_items: 1_000_000, format: "json"
  } #: verify_options
  parser = OptionParser.new do |options|
    options.banner = "Usage: ibex verify [options] AUTOMATON.json"
    options.on("--strict", "include completeness and table-bisimulation checks") { settings[:strict] = true }
    options.on("--grammar=GRAMMAR", "require an exact embedded Grammar IR match") do |value|
      settings[:grammar] = value
    end
    options.on("--max-states=N", Integer, "maximum independently derived states") do |value|
      settings[:max_states] = positive_verify_budget(value, "max-states")
    end
    options.on("--max-items=N", Integer, "maximum independently derived items") do |value|
      settings[:max_items] = positive_verify_budget(value, "max-items")
    end
    options.on("--format=FORMAT", %w[json text], "json or text") { |value| settings[:format] = value }
    options.on("--help", "show help") { settings[:help] = options.to_s }
  end
  settings[:paths] = parser.parse(arguments)
  settings
end

#verify_supplied_grammar!(automaton, path) ⇒ void

This method returns an undefined value.

RBS:

  • (IR::Automaton automaton, String path) -> void

Parameters:



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

def verify_supplied_grammar!(automaton, path)
  value = IR::Validator.validate(File.binread(path))
  raise Ibex::Error, "#{path}:1:1: --grammar requires Grammar IR" unless value.is_a?(IR::Grammar)
  return if IR::Serialize.dump(value) == IR::Serialize.dump(automaton.grammar)

  raise Ibex::Error, "#{path}:1:1: Grammar IR does not match the automaton's embedded grammar"
end

#write_verify_result(result, format) ⇒ void

This method returns an undefined value.

RBS:

  • (Verify::Result result, String format) -> void

Parameters:



97
98
99
100
101
102
103
104
105
106
107
 
# File 'lib/ibex/cli/verify.rb', line 97

def write_verify_result(result, format)
  if format == "json"
    @stdout.puts(JSON.pretty_generate(result.to_h))
    return
  end

  @stdout.puts("result=#{result.valid? ? 'valid' : 'invalid'} algorithm=#{result.algorithm}")
  result.violations.each do |violation|
    @stdout.puts("#{violation.id} #{violation.location}: #{violation.message}")
  end
end